avewright/proofwiki-math huggingface dataset:
Theorem: Combination Theorem for Continuous Mappings/Normed Division Ring/Sum Rule

:$f + g: \struct {S, \tau_{_S} } \to \struct{R, \tau_{_R} }$ is continuous.

Proof:
From {{Corollary|Normed Division Ring Operations are Continuous}}:
:$\struct {R, +, *, \tau_{_R} }$ is a topological division ring.
From Sum Rule for Continuous Mappings to Topological Division Ring:
:$f + g: \struct {S, \tau_{_S} } \to \struct {R, \tau_{_R} }$ is a continuous mapping.
{{qed}}
Theorem: Combination Theorem for Continuous Mappings/Normed Division Ring/Multiple Rule

:$\lambda * f: \struct {S, \tau_{_S} } \to \struct {R, \tau_{_R} }$ is continuous
:$f * \lambda: \struct {S, \tau_{_S} } \to \struct {R, \tau_{_R} }$ is continuous.

Proof:
From {{Corollary|Normed Division Ring Operations are Continuous}}:
:$\struct {R, +, *, \tau_{_R} }$ is a topological division ring.
From Multiple Rule for Continuous Mappings to Topological Division Ring:
:$\lambda * f, f * \lambda: \struct {S, \tau_{_S} } \to \struct {R, \tau_{_R} }$ are continuous mappings.
{{qed}}
Theorem: Combination Theorem for Continuous Mappings/Normed Division Ring/Product Rule

:$f * g: \struct {S, \tau_{_S} } \to \struct {R, \tau_{_R} }$ is continuous.

Proof:
From {{Corollary|Normed Division Ring Operations are Continuous}}:
:$\struct {R, +, *, \tau_{_R} }$ is a topological division ring.
From Product Rule for Continuous Mappings to Topological Division Ring:
:$f * g: \struct {S, \tau_{_S} } \to \struct {R, \tau_{_R} }$ is a continuous mapping.
{{qed}}
Theorem: Combination Theorem for Continuous Mappings/Normed Division Ring/Inverse Rule

:$g^{-1}: \struct {U, \tau_{_U} } \to \struct {R, \tau_{_R} }$ is continuous.

Proof:
From {{Corollary|Normed Division Ring Operations are Continuous}}:
:$\struct {R, +, *, \tau_{_R} }$ is a topological division ring.
From Inverse Rule for Continuous Mappings to Topological Division Ring:
:$g^{-1}: \struct {U, \tau_{_U} } \to \struct {R, \tau_{_R} }$ is a continuous mapping.
{{qed}}
Theorem: Definite Integral to Infinity of x by Sine m x over x Squared plus a Squared

:$\ds \int_0^\infty \frac {x \sin m x} {x^2 + a^2} \rd x = \frac \pi 2 e^{-m a}$

Proof:
From Definite Integral to Infinity of $\dfrac {\cos m x} {x^2 + a^2}$:
:$\ds \int_0^\infty \frac {\cos m x} {x^2 + a^2} \rd x = \frac \pi {2 a} e^{-m a}$
We have: 
{{begin-eqn}}
{{eqn	| l = \frac \d {\d m} \int_0^\infty \frac {\cos m x} {x^2 + a^2} \rd x
	| r = \int_0^\infty \frac \partial {\partial m} \paren {\frac {\cos m x} {x^2 + a^2} } \rd x
	| c = Definite Integral of Partial Derivative
}}
{{eqn	| r = -\int_0^\infty \frac {x \sin m x} {x^2 + a^2} \rd x
	| c = Derivative of $\cos a x$
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac {x \sin m x} {x^2 + a^2} \rd x
	| r = -\frac \d {\d m} \paren {\frac \pi {2 a} e^{-m a} }
}}
{{eqn	| r = \frac \pi 2 e^{-m a}
	| c = Derivative of $e^{a x}$
}}
{{end-eqn}}
{{qed}}
Theorem: Power Series Expansion for Cosine Integral Function

{{begin-eqn}}
{{eqn | l = \map \Ci x
      | r = -\gamma - \ln x + \sum_{n \mathop = 1}^\infty \paren {-1}^{n + 1} \frac {x^{2 n} } {\paren {2 n} \times \paren {2 n}!}
      | c = 
}}
{{eqn | r = -\gamma - \ln x + \dfrac {x^2} {2 \cdot 2!} - \dfrac {x^4} {4 \cdot 4!} + \dfrac {x^6} {6 \cdot 6!} - \dfrac {x^8} {8 \cdot 8!} + \cdots
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map \Ci x
      | r = -\gamma - \ln x + \int_0^x \frac {1 - \cos u} u \rd u
      | c = Characterization of Cosine Integral Function
}}
{{eqn | r = -\gamma - \ln x + \int_0^x \frac 1 u \paren {1 - \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {u^{2 n} } {\paren {2 n}!} } \rd u
      | c = Power Series Expansion for Cosine Function
}}
{{eqn | r = -\gamma - \ln x + \sum_{n \mathop = 1}^\infty \paren {-1}^{n + 1} \int_0^x \frac {u^{2 n - 1} } {\paren {2 n}!} \rd u
      | c = Power Series is Termwise Integrable within Radius of Convergence
}}
{{eqn | r = -\gamma - \ln x + \sum_{n \mathop = 1}^\infty \paren {-1}^{n + 1} \frac {u^{2 n} } {\paren {2 n} \times \paren {2 n}!}
      | c = Primitive of Power
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Cosine Integral Function

:$\dfrac \d {\d x} \paren {\map \Ci x} = -\dfrac {\cos x} x$

Proof:
{{begin-eqn}}
{{eqn	| l = \frac \d {\d x} \paren {\map \Ci x}
	| r = \frac \d {\d x} \paren {-\gamma - \ln x + \int_0^x \frac {1 - \cos t} t \rd t}
	| c = Characterization of Cosine Integral Function
}}
{{eqn	| r = -\frac 1 x + \frac 1 x - \frac {\cos x} x
	| c = Derivative of Constant, Derivative of Natural Logarithm, Fundamental Theorem of Calculus: First Part (Corollary)
}}
{{eqn	| r = -\frac {\cos x} x
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Exponential Integral Function

Let $\Ei: \R_{>0} \to \R$ denote the exponential integral function:
:$\map \Ei x = \ds \int_{t \mathop = x}^{t \mathop \to +\infty} \frac {e^{-t} } t \rd t$
Then:
:$\dfrac \d {\d x} \paren {\map \Ei x} = -\dfrac {e^{-x} } x$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {\map \Ei x}
      | r = \map {\frac \d {\d x} } {-\gamma - \ln x + \int_0^x \frac {1 - e^{-t} } t \rd t}
      | c = Characterization of Exponential Integral Function
}}
{{eqn | r = -\frac 1 x + \frac 1 x - \frac {e^{-x} } x
      | c = Derivative of Constant, Derivative of Natural Logarithm, Fundamental Theorem of Calculus: First Part (Corollary)
}}
{{eqn | r = -\frac {e^{-x} } x
}}
{{end-eqn}}
{{qed}}
Category:Derivatives
Category:Exponential Integral Function
gsfy8kueyp9ckpeqwhrr7qpdw9k2lld
Theorem: Derivative of Sine Integral Function

:$\dfrac \d {\d x} \paren {\map \Si x} = \dfrac {\sin x} x$

Proof:
We have, by the definition of the sine integral function: 
:$\ds \map \Si x = \int_0^x \frac {\sin t} t \rd t$
By {{Corollary|Fundamental Theorem of Calculus/First Part|disp = Fundamental Theorem of Calculus (First Part)}}, we  have: 
:$\ds \frac \d {\d x} \paren {\map \Si x} = \frac {\sin x} x$
{{qed}}
Theorem: Primitive of Cosine Integral Function

:$\ds \int \map \Ci x \rd x = x \map \Ci x + \sin x + C$

Proof:
By Derivative of Cosine Integral Function, we have: 
:$\ds \frac \d {\d x} \paren {\map \Ci x} = -\frac {\cos x} x$
So:
{{begin-eqn}}
{{eqn	| l = \int \map \Ci x \rd x
	| r = \int 1 \times \map \Ci \rd x
}}
{{eqn	| r = x \map \Ci x - \int \paren {-x \frac {\cos x} x} \rd x
	| c = Integration by Parts
}}
{{eqn	| r = x \map \Ci x + \int \cos x \rd x
}}
{{eqn	| r = x \map \Ci x + \sin x + C
	| c = Primitive of Cosine Function
}}
{{end-eqn}}
{{qed}}
Category:Primitives
Category:Cosine Integral Function
53d3rklsenqk9gbmcgr0ouh13sfiyh7
Theorem: Primitive of Exponential Integral Function

Let $\Ei: \R_{>0} \to \R$ denote the exponential integral function:
:$\map \Ei x = \ds \int_{t \mathop = x}^{t \mathop \to +\infty} \frac {e^{-t} } t \rd t$
Then:
:$\ds \int \map \Ei x \rd x = x \map \Ei x - e^{-x} + C$

Proof:
By Derivative of Exponential Integral Function, we have: 
:$\ds \frac \d {\d x} \paren {\map \Ei x} = -\frac {e^{-x} } x$
So: 
{{begin-eqn}}
{{eqn | l = \int \map \Ei x \rd x
      | r = \int 1 \times \map \Ei x \rd x
}}
{{eqn | r = x \map \Ei x - \int \paren {-x \frac {e^{-x} } x} \rd x
      | c = Integration by Parts
}}
{{eqn | r = x \map \Ei x + \int e^{-x} \rd x
}}
{{eqn | r = x \map \Ei x - e^{-x} + C
      | c = Primitive of $e^{a x}$
}}
{{end-eqn}}
{{qed}}
Category:Primitives
Category:Exponential Integral Function
607ffw7hkqdd7bsnjndabd5gi0sr248
Theorem: Direct Image Mapping of Domain is Image Set of Mapping

Let $S$ and $T$ be sets.
Let $\powerset S$ and $\powerset T$ be their power sets.
Let $f \subseteq S \times T$ be a mapping from $S$ to $T$.
Let $f^\to: \powerset S \to \powerset T$ be the direct image mapping of $f$:
:$\forall X \in \powerset S: \map {f^\to} X = \begin {cases} \set {t \in T: \exists s \in X: \map f s = t} & : X \ne \O \\ \O & : X = \O \end {cases}$
Then:
:$\map {f^\to} S = \Img f$
where $\Img f$ is the image set of $f$.

Proof:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \map {f^\to} S
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists x \in S
      | l = \map f x
      | r = y
      | c = {{Defof|Direct Image Mapping of Mapping}}
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | o = \in
      | r = \Img f
      | c = {{Defof|Image Set of Mapping}}
}}
{{end-eqn}}
{{Qed}}
Category:Direct Image Mappings
515nxse6ynpcqvbp75c188siiptdzeq
Theorem: Direct Image Mapping of Domain is Image Set of Relation

Let $S$ and $T$ be sets.
Let $\powerset S$ and $\powerset T$ be their power sets.
Let $\RR \subseteq S \times T$ be a relation on $S \times T$.
Let $\RR^\to: \powerset S \to \powerset T$ be the direct image mapping of $\RR$:
:$\forall X \in \powerset S: \map {\RR^\to} X = \begin {cases} \set {t \in T: \exists s \in X: \tuple {x, t} \in \RR} & : X \ne \O \\ \O & : X = \O \end {cases}$
Then:
:$\map {\RR^\to} {\Dom \RR} = \Img \RR$
where:
:$\Dom \RR$ is the domain of $\RR$
:$\Img \RR$ is the image set of $\RR$.

Proof:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \map {\RR^\to} {\Dom \RR}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists x \in S
      | l = \tuple {x, y}
      | o = \in
      | r = \RR
      | c = {{Defof|Direct Image Mapping of Mapping}}
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | o = \in
      | r = \Img \RR
      | c = {{Defof|Image Set of Relation}}
}}
{{end-eqn}}
{{Qed}}
Category:Direct Image Mappings
hlavned44m7fd5ofhupl1zzzl190fdv
Theorem: Inverse Image Mapping of Codomain is Preimage Set of Mapping

Let $S$ and $T$ be sets.
Let $\powerset S$ and $\powerset T$ be their power sets.
Let $f \subseteq S \times T$ be a mapping from $S$ to $T$.
Let $f^\gets: \powerset T \to \powerset S$ be the inverse image mapping of $f$:
:$\forall Y \in \powerset T: \map {f^\gets} Y = \begin {cases} \set {s \in S: \exists t \in Y: \map f s = t} & : \Img f \cap Y \ne \O \\ \O & : \Img f \cap Y = \O \end {cases}$
Then:
:$\map {f^\gets} T = \Preimg f$
where $\Preimg f$ is the preimage set of $f$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \map {f^\gets} T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists y \in T
      | l = \map f x
      | r = y
      | c = {{Defof|Inverse Image Mapping of Mapping}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \Preimg f
      | c = {{Defof|Preimage Set of Mapping}}
}}
{{end-eqn}}
{{Qed}}
Category:Inverse Image Mappings
m8pi7xi8ir3dfcshjth8xlexz1ou1jf
Theorem: Inverse Image Mapping of Codomain is Preimage Set of Relation

Let $S$ and $T$ be sets.
Let $\powerset S$ and $\powerset T$ be their power sets.
Let $\RR \subseteq S \times T$ be a relation on $S \times T$.
Let $\RR^\gets: \powerset T \to \powerset S$ be the inverse image mapping of $\RR$:
:$\forall X \in \powerset S: \map {\RR^\to} X = \begin {cases} \set {t \in T: \exists s \in X: \tuple {x, t} \in \RR} & : X \ne \O \\ \O & : X = \O \end {cases}$
Then:
:$\map {\RR^\gets} T = \Preimg \RR$
where $\Preimg \RR$ is the preimage of $\RR$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \map {\RR^\gets} T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists x \in S
      | l = \tuple {x, y}
      | o = \in
      | r = \RR
      | c = {{Defof|Inverse Image Mapping of Mapping}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \Preimg \RR
      | c = {{Defof|Preimage of Relation}}
}}
{{end-eqn}}
{{Qed}}
Category:Inverse Image Mappings
h00hu7lkdltv3bdmpidj8o7j4r62ap2
Theorem: Direct Image Mapping of Mapping is Mapping

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping on $S \times T$.
Let $f^\to: \powerset S \to \powerset T$ be the direct image mapping of $f$:
:$\forall X \in \powerset S: \map {f^\to} X = \set {t \in T: \exists s \in X: \map f s = t}$
Then $f^\to$ is indeed a mapping.

Proof:
$f$, being a mapping, is also a relation.
Hence Direct Image Mapping of Relation is Mapping can be applied directly.
{{qed}}
Theorem: Inverse Image Mapping of Mapping is Mapping

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping from $S$ to $T$.
Let $f^\gets$ be the inverse image mapping of $f$:
:$f^\gets: \powerset T \to \powerset S: \map {f^\gets} Y = f^{-1} \sqbrk Y$
Then $f^\gets$ is indeed a mapping.

Proof:
$f^{-1}$ is a relation.
So Inverse Image Mapping of Relation is Mapping applies directly.
{{qed}}
Theorem: Direct Image Mapping of Mapping is Empty iff Argument is Empty

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping from $S$ to $T$.
Let $f^\to$ be the direct image mapping of $f$:
:$f^\to: \powerset S \to \powerset T: \map {f^\to} X = \set {t \in T: \exists s \in X: \map f s = t}$
Then:
:$\map {f^\to} X = \O \iff X = \O$

Proof:
By definition, a mapping is a left-total relation.
The result then follows from Direct Image Mapping of Left-Total Relation is Empty iff Argument is Empty.
{{qed}}
Theorem: Derivative of Fresnel Sine Integral Function

:$\dfrac {\d \mathrm S} {\d x} = \sqrt {\dfrac 2 \pi} \sin x^2$

Proof:
We have, by the definition of the Fresnel sine integral function:
:$\ds \map {\mathrm S} x = \sqrt {\frac 2 \pi} \int_0^x \sin u^2 \rd u$
By Fundamental Theorem of Calculus (First Part): Corollary, we therefore have:
:$\dfrac {\d \mathrm S} {\d x} = \sqrt {\dfrac 2 \pi} \sin x^2$
{{qed}}
Category:Fresnel Sine Integral Function
Category:Derivatives
pvjjgqu68w7vk8q4d8dtm2dlo13ycth
Theorem: Derivative of Fresnel Cosine Integral Function

:$\dfrac {\d \mathrm C} {\d x} = \sqrt {\dfrac 2 \pi} \cos x^2$

Proof:
We have, by the definition of the Fresnel cosine integral function:
:$\ds \map {\mathrm C} x = \sqrt {\dfrac 2 \pi} \int_0^x \cos u^2 \rd u$
By Fundamental Theorem of Calculus (First Part): Corollary, we therefore have:
:$\dfrac {\d \mathrm C} {\d x} = \sqrt {\dfrac 2 \pi} \cos x^2$
{{qed}}
Category:Fresnel Cosine Integral Function
Category:Derivatives
kr2o471065p5jgizh72cw3lunh029hf
Theorem: Power Series Expansion for Fresnel Sine Integral Function

{{begin-eqn}}
{{eqn | l = \map {\operatorname S} x
      | r = \sqrt {\frac 2 \pi} \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{4 n + 3} } {\paren {4 n + 3} \paren {2 n + 1}!}
      | c = 
}}
{{eqn | r = \sqrt {\frac 2 \pi} \paren {\dfrac {x^3} {3 \cdot 1!} - \dfrac {x^7} {7 \cdot 3!} + \dfrac {x^{11} } {11 \cdot 5!} - \dfrac {x^{15} } {15 \cdot 7!} + \cdots}
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map {\operatorname S} x
      | r = \sqrt {\frac 2 \pi} \int_0^x \sin u^2 \rd u
      | c = {{Defof|Fresnel Sine Integral Function}}
}}
{{eqn | r = \sqrt {\frac 2 \pi} \int_0^x \paren {\sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {\paren {u^2}^{2 n + 1} } {\paren {2 n + 1}!} } \rd u
      | c = Power Series Expansion for Sine Function
}}
{{eqn | r = \sqrt {\frac 2 \pi} \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n} {\paren {2 n + 1}!} \int_0^x u^{4 n + 2} \rd u
      | c = Power Series is Termwise Integrable within Radius of Convergence
}}
{{eqn | r = \sqrt {\frac 2 \pi} \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{4 n + 3} } {\paren {4 n + 3} \paren {2 n + 1}!}
      | c = Primitive of Power
}}
{{end-eqn}}
{{qed}}
Theorem: Power Series Expansion for Fresnel Cosine Integral Function

{{begin-eqn}}
{{eqn | l = \map {\operatorname C} x
      | r = \sqrt {\frac 2 \pi} \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{4 n + 1} } {\paren {4 n + 1} \paren {2 n}!}
      | c = 
}}
{{eqn | r = \sqrt {\frac 2 \pi} \paren {\dfrac x {1!} - \dfrac {x^5} {5 \cdot 2!} + \dfrac {x^9} {9 \cdot 4!} - \dfrac {x^{13} } {13 \cdot 6!} + \cdots}
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map {\operatorname C} x 
      | r = \sqrt {\frac 2 \pi} \int_0^x \cos u^2 \rd u
      | c = {{Defof|Fresnel Cosine Integral Function}}
}}
{{eqn | r = \sqrt {\frac 2 \pi} \int_0^x \paren {\sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {\paren {u^2}^{2 n} } {\paren {2 n}!} } \rd u
      | c = Power Series Expansion for Cosine Function
}}
{{eqn | r = \sqrt {\frac 2 \pi} \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n} {\paren {2 n}!} \int_0^x u^{4 n} \rd u
      | c = Power Series is Termwise Integrable within Radius of Convergence
}}
{{eqn | r = \sqrt {\frac 2 \pi} \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{4 n + 1} } {\paren {4 n + 1} \paren {2 n}!}
      | c = Primitive of Power
}}
{{end-eqn}}
{{qed}}
Theorem: Fresnel Sine Integral Function is Odd

:$\map {\operatorname S} {-x} = -\map {\operatorname S} x$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\operatorname S} {-x}
      | r = \sqrt {\frac 2 \pi} \int_0^{-x} \sin u^2 \rd u
      | c = {{Defof|Fresnel Sine Integral Function}}
}}
{{eqn | r = -\sqrt {\frac 2 \pi} \int_0^{-\paren {-x} } \map \sin {\paren {-u}^2} \rd u
      | c = substituting $u \mapsto -u$
}}
{{eqn | r = -\sqrt {\frac 2 \pi} \int_0^x \sin u^2 \rd u
}}
{{eqn | r = -\map {\operatorname S} x
      | c = {{Defof|Fresnel Sine Integral Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Fresnel Sine Integral Function of Zero

:$\map {\operatorname S} 0 = 0$

Proof:
By Fresnel Sine Integral Function is Odd, $\operatorname S$ is an odd function.
Therefore, by Odd Function of Zero is Zero:
:$\map {\operatorname S} 0 = 0$
{{qed}}
Theorem: Limit to Infinity of Fresnel Sine Integral Function

:$\ds \lim_{x \mathop \to \infty} \map {\mathrm S} x = \frac 1 2$

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to \infty} \map {\mathrm S} x
      | r = \sqrt {\frac 2 \pi} \lim_{x \mathop \to \infty} \int_0^x \sin u^2 \rd u
      | c = Multiple Rule for Limits of Real Functions, {{Defof|Fresnel Sine Integral Function}}
}}
{{eqn | r = \sqrt {\frac 2 \pi} \int_0^\infty \sin u^2 \rd u
}}
{{eqn | r = \sqrt {\frac 2 \pi} \times \frac 1 2 \sqrt {\frac \pi 2}
      | c = Definite Integral to Infinity of $\map \sin {a x^2}$
}}
{{eqn | r = \frac 1 2
}}
{{end-eqn}}
{{qed}}
Theorem: Asymptotic Expansion for Fresnel Sine Integral Function

:$\map {\operatorname S} x \sim \dfrac 1 2 - \dfrac 1 {\sqrt {2 \pi} } \paren {\map \cos {x^2} \paren {\dfrac 1 x - \dfrac {1 \times 3} {2^2 x^5} + \dfrac {1 \times 3 \times 5 \times 7} {2^4 x^9} - \ldots} + \map \sin {x^2} \paren {\dfrac 1 {2 x^3} - \dfrac {1 \times 3 \times 5} {2^3 x^7} + \ldots} }$

Proof:
{{ProofWanted|also establish general term and write sums with $\sum$}}
Theorem: Fresnel Cosine Integral Function is Odd

:$\map {\operatorname C} {-x} = -\map {\operatorname C} x$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\operatorname C} {-x}
      | r = \sqrt {\frac 2 \pi} \int_0^{-x} \cos u^2 \rd u
      | c = {{Defof|Fresnel Cosine Integral Function}}
}}
{{eqn | r = -\sqrt {\frac 2 \pi} \int_0^{-\paren {-x} } \map \cos {\paren {-u}^2} \rd u
      | c = substituting $u \mapsto -u$
}}
{{eqn | r = -\sqrt {\frac 2 \pi} \int_0^x \cos u^2 \rd u
}}
{{eqn | r = -\map {\operatorname C} x
      | c = {{Defof|Fresnel Cosine Integral Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Fresnel Cosine Integral Function of Zero

:$\map {\operatorname C} 0 = 0$

Proof:
By Fresnel Cosine Integral Function is Odd, $\operatorname C$ is an odd function.
Therefore, by Odd Function of Zero is Zero:
:$\map {\operatorname C} 0 = 0$
{{qed}}
Theorem: Direct Image Mapping of Left-Total Relation is Empty iff Argument is Empty

Let $S$ and $T$ be sets.
Let $\RR: S \to T$ be a left-total relation on $S \times T$.
Let $\RR^\to$ be the direct image mapping of $\RR$:
:$\RR^\to: \powerset S \to \powerset T: \map {\RR^\to} X = \set {t \in T: \exists s \in X: \tuple {s, t} \in \RR}$
Then:
:$\map {\RR^\to} X = \O \iff X = \O$

Proof:
=== Sufficient Condition ===
Let $\map {\RR^\to} X = \O$.
By definition of direct image mapping:
:$\set {t \in T: \exists s \in X: \tuple {s, t} \in \RR} = \O$
That is:
:$\neg \exists s \in X: \tuple {s, t} \in \RR$
But as $\RR$ is a left-total relation:
:$\forall s \in X: \exists t \in T: \tuple {s, t} \in \RR$
Thus:
:$\neg \exists s \in X$
and so:
:$X = \O$
{{qed|lemma}}
Theorem: Limit to Infinity of Fresnel Cosine Integral Function

:$\ds \lim_{x \mathop \to \infty} \map {\mathrm C} x = \frac 1 2$

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to \infty} \map {\mathrm C} x
      | r = \sqrt {\frac 2 \pi} \lim_{x \mathop \to \infty} \int_0^x \cos u^2 \rd u
      | c = Multiple Rule for Limits of Real Functions, {{Defof|Fresnel Cosine Integral Function}}
}}
{{eqn | r = \sqrt {\frac 2 \pi} \int_0^\infty \cos u^2 \rd u
}}
{{eqn | r = \sqrt {\frac 2 \pi} \times \frac 1 2 \sqrt {\frac \pi 2}
      | c = Definite Integral to Infinity of $\map \cos {a x^2}$
}}
{{eqn | r = \frac 1 2
}}
{{end-eqn}}
{{qed}}
Theorem: Successor Mapping on Natural Numbers is not Surjection

Let $f: \N \to \N$ be the successor mapping on the natural numbers $\N$:
:$\forall n \in \N: \map f n = n + 1$
Then $f$ is not a surjection.

Proof:
There exists no $n \in \N$ such that $n + 1 = 0$.
Thus $\map f 0$ has no preimage.
The result follows by definition of surjection.
{{qed}}
Theorem: Composition of Direct Image Mappings of Mappings

Let $A, B, C$ be non-empty sets.
Let $f: A \to B$ and $g: B \to C$ be mappings.
Let:
:$f^\to: \powerset A \to \powerset B$
and
:$g^\to: \powerset B \to \powerset C$
be the direct image mappings of $f$ and $g$.
Then:
:$\paren {g \circ f}^\to = g^\to \circ f^\to$

Proof:
Let $S \subseteq A$ such that $S \ne \O$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren {g^\to \circ f^\to} } S
      | r = \map {g^\to} {\map {f^\to} S}
      | c = 
}}
{{eqn | r = \set {\map g x: x \in \map {f^\to} S}
      | c = 
}}
{{eqn | r = \set {\map g x: \exists y \in S: x = \map f y}
      | c = 
}}
{{eqn | r = \set {\map g {\map f y}: y \in S}
      | c = 
}}
{{eqn | r = \set {\map {\paren {g \circ f} } y: y \in S}
      | c = 
}}
{{eqn | r = \map {\paren {g \circ f}^\to} S
      | c = 
}}
{{end-eqn}}
Now we treat the case where $S = \O$:
{{begin-eqn}}
{{eqn | l = \map {\paren {g^\to \circ f^\to} } \O
      | r = \O
      | c = 
}}
{{eqn | r = \map {\paren {g \circ f}^\to} \O
      | c = 
}}
{{end-eqn}}
and the result is complete.
{{qed}}
Theorem: Composition of Inverse Image Mappings of Mappings

Let $A, B, C$ be non-empty sets.
Let $f: A \to B, g: B \to C$ be mappings.
Let:
:$f^\gets: \powerset B \to \powerset A$
and
:$g^\gets: \powerset C \to \powerset B$
be the inverse image mappings of $f$ and $g$.
Then:
:$\paren {g \circ f}^\gets = f^\gets \circ g^\gets$

Proof:
Let $T \subseteq C$.
We have:
{{begin-eqn}}
{{eqn | l = \map {\paren {f \circ g}^\gets} T
      | r = \begin {cases} \set {x \in A: \map g {\map f x} \in T} & : \Img {g \circ f} \cap T \ne \O \\ \O & : \Img {g \circ f} \cap T = \O \end {cases}
      | c = 
}}
{{eqn-intertext|and}}
{{eqn | l = \map {f^\gets \circ g^\gets} T
      | r = \begin {cases} \set {x \in A: \map f x \in \map {g^\gets} T} & : \Img f \cap \map {g^\gets} T \ne \O \\ \O & : \Img f \cap \map {g^\gets} T = \O \end {cases}
      | c = 
}}
{{eqn | r = \begin {cases} \set {x \in A: \map g {\map f x} \in T} & : \Img f \cap \map {g^\gets} T \ne \O \\ \O & : \Img f \cap \map {g^\gets} T = \O \end {cases}
      | c = 
}}
{{end-eqn}}
It remains to be shown that:
:$\Img f \cap \map {g^\gets} T = \O \iff \Img {g \circ f} \cap T = \O$
So:
{{begin-eqn}}
{{eqn | l = \Img f \cap \map {g^\gets} T
      | r = \O
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \Img f
      | o = \subseteq
      | r = \relcomp B {\map {g^\gets} T}
      | c = Empty Intersection iff Subset of Complement
}}
{{eqn | r = \map {g^\gets} {\relcomp C T}
      | c = Complement of Preimage equals Preimage of Complement
}}
{{eqn | ll= \leadstoandfrom
      | l = \Img {g \circ f}
      | r = \map {g^\gets} {\Img f}
      | c = Intersection with Complement is Empty iff Subset
}}
{{eqn | o = \subseteq
      | r = \relcomp C T
      | c = Subset of Preimage under Relation is Preimage of Subset: Corollary
}}
{{eqn | ll= \leadstoandfrom
      | l = \Img {g \circ f} \cap T
      | r = \O
      | c = Empty Intersection iff Subset of Complement
}}
{{end-eqn}}
{{qed}}