\chapter{Explicit Reals II and Fields}
\section{explicit\_Reals}\label{fgihahmgjgdgjgehpfcffgbgmgdh}Let $ R : {\iota}$ be given.
Let $ zero one : {\iota}$ be given.
Let $ plus mult : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${plus}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${mult}$.
{\bf{Notation.}} We use $\prenc{-}$ as a prefix operator  corresponding to applying term ${{{{{{\mname{explicit\_Field\_minus}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}$.
Let $ leq : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ be given.
{\bf{Notation.}} We use $\infmdnd$ as an infix operator  corresponding to applying term ${leq}$.
Let $N$ be ${\{n \in {R}|{{{{{{{{\mname{natOfOrderedField\_p}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}~{n}}\}}$.
Let $Npos$ be ${\{n \in {N}|{{n}\unicdcdgdad{zero}}\}}$.
Let $Z$ be ${\{n \in {R}|{{{{\prenc{{n}}} \in {Npos}}\unicdcdcdid{{n}={zero}}}\unicdcdcdid{{n} \in {Npos}}}\}}$.
Let $Q$ be ${\{x \in {R}|{{{{{{{{\mname{explicit\_OrderedField\_rationalp}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}~{x}}\}}$.
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpffgihahmgjgdgjgehpfgejgfgmgegpfbf} ${{{{{{{{\mname{explicit\_OrderedField}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}\unicdbdjdcd{{{{{{\mname{explicit\_Field}}~{Q}}~{zero}}~{one}}~{plus}}~{mult}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & af6a3ba60f48d142602c8b680df2961966f1dca1044d4270f1f29c8a72c59c21 \\
Pure Prop Address: & TMZT73ZmoriPCPWsoj29MFJq3aK7fa41ff9 \\
Theory Prop Id: & 63d4c7bfde12c187c511272b653382138f0591cd1d246d9947331032fefa5c86 \\
Theory Prop Address: & TMGnn2Z2r22We9QuK5hXYB6c9XHixx14xDr
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfdhfhcg} ${{{{{{{{\mname{explicit\_OrderedField}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}\unicdbdjdcd{\unicdcdadad R' \subseteq {R} .  {{{zero} \in {R'}}\unicdbdjdcd{{{one} \in {R'}}\unicdbdjdcd{{({\unicdcdadad x y \in {R'} .  {{{x}+{y}} \in {R'}}})}\unicdbdjdcd{{({\unicdcdadad x \in {R'} .  {{\prenc{{x}}} \in {R'}}})}\unicdbdjdcd{{({\unicdcdadad x y \in {R'} .  {{{x}*{y}} \in {R'}}})}\unicdbdjdcd{{({\unicdcdadad x \in {R'} .  {{{x}\unicdcdgdad{zero}}\unicdbdjdcd{\unicdcdaddd y \in {R'} .  {{{x}*{y}}={one}}}}})}\unicdbdjdcd{{{{{{{\mname{explicit\_OrderedField}}~{R'}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1bc19ee4bcca58ce8b4534af0101d211b4fc533dc4db649a1bb010477c1d0998 \\
Pure Prop Address: & TMF49guKUWG2dHumcM9HEv55USiZpXFGiDg \\
Theory Prop Id: & 9966383d1240a949659da39081fa3506cca4e377a161c6ab8ff8c05865a2eab3 \\
Theory Prop Address: & TMLR4J2wofUrAHouvRF1dws9BDPmZefs7gr
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcffgbgmgdhpfdhfhcg} ${{{{{{{{\mname{explicit\_OrderedField}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}\unicdbdjdcd{\unicdcdadad R' \subseteq {R} .  {{{zero} \in {R'}}\unicdbdjdcd{{{one} \in {R'}}\unicdbdjdcd{{({\unicdcdadad x y \in {R'} .  {{{x}+{y}} \in {R'}}})}\unicdbdjdcd{{({\unicdcdadad x \in {R'} .  {{\prenc{{x}}} \in {R'}}})}\unicdbdjdcd{{({\unicdcdadad x y \in {R'} .  {{{x}*{y}} \in {R'}}})}\unicdbdjdcd{{({\unicdcdadad x \in {R'} .  {{{x}\unicdcdgdad{zero}}\unicdbdjdcd{\unicdcdaddd y \in {R'} .  {{{x}*{y}}={one}}}}})}\unicdbdjdcd{{{{{{{\mname{explicit\_OrderedField}}~{R'}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1bc19ee4bcca58ce8b4534af0101d211b4fc533dc4db649a1bb010477c1d0998 \\
Pure Prop Address: & TMF49guKUWG2dHumcM9HEv55USiZpXFGiDg \\
Theory Prop Id: & 9966383d1240a949659da39081fa3506cca4e377a161c6ab8ff8c05865a2eab3 \\
Theory Prop Address: & TMLR4J2wofUrAHouvRF1dws9BDPmZefs7gr
\end{tabular}
\end{center}

\end{theorem}
\subsection{explicit\_Reals\_Q\_min\_props}\label{fgihahmgjgdgjgehpfcffgbgmgdhpfbfpfngjgogpfahchpgahdh}Let $ R' : {\iota}$ be given.
Let $N'$ be ${\{n \in {R'}|{{{{{{{{\mname{natOfOrderedField\_p}}~{R'}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}~{n}}\}}$.
Let $Npos'$ be ${\{n \in {N'}|{{n}\unicdcdgdad{zero}}\}}$.
Let $Z'$ be ${\{n \in {R'}|{{{{{{{{{{\mname{explicit\_Field\_minus}}~{R'}}~{zero}}~{one}}~{plus}}~{mult}}~{n}} \in {Npos'}}\unicdcdcdid{{n}={zero}}}\unicdcdcdid{{n} \in {Npos'}}}\}}$.
Let $Q'$ be ${\{x \in {R'}|{{{{{{{{\mname{explicit\_OrderedField\_rationalp}}~{R'}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}~{x}}\}}$.
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcffgbgmgdhpfbfpfngjgogpfahchpgahdh} ${{{{{{{{\mname{explicit\_OrderedField}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}\unicdbdjdcd{{{R'} \subseteq {R}}\unicdbdjdcd{{{{{{{\mname{explicit\_Field}}~{R'}}~{zero}}~{one}}~{plus}}~{mult}}\unicdbdjdcd{\unicdcdadad p : {o} .  {{({{({\unicdcdadad x \in {R'} .  {{{{{{{{\mname{explicit\_Field\_minus}}~{R'}}~{zero}}~{one}}~{plus}}~{mult}}~{x}}={\prenc{{x}}}}})}\unicdbdjdcd{{({\unicdcdadad x \in {R'} .  {{\prenc{{x}}} \in {R'}}})}\unicdbdjdcd{{{N}={N'}}\unicdbdjdcd{{{Npos}={Npos'}}\unicdbdjdcd{{{Z}={Z'}}\unicdbdjdcd{{{Q}={Q'}}\unicdbdjdcd{p}}}}}}})}\unicdbdjdcd{p}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 31679e3e73614c3b4e276ed2c828816866f95e9a6a5e2f4721f319e80f473912 \\
Pure Prop Address: & TMLPtuuQw2TanZmHDBpjYzPS2V2V5uY5Rv5 \\
Theory Prop Id: & 2ead4f461950b2019d11d00ddc1a62977823328b7794ed17307fb66dde3d0ccf \\
Theory Prop Address: & TMU33ZE5CuhCrg8XK3QNyMjHM54qa6M4HFy
\end{tabular}
\end{center}

\end{theorem}
\subsection{Q is Minimal as a Subfield of R} % explicit_Reals_Q_min_props
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcffgbgmgdhpfbfpfngjgog} ${{{{{{{{\mname{explicit\_OrderedField}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}\unicdbdjdcd{\unicdcdadad R' \subseteq {R} .  {{{{{{{\mname{explicit\_Field}}~{R'}}~{zero}}~{one}}~{plus}}~{mult}}\unicdbdjdcd{{Q} \subseteq {R'}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & aa9362c28b55f5ede37059e938f69a0bdc1f5a2c40ebc1e5233c99544f022cfc \\
Pure Prop Address: & TMTBsyn4r1w2A2v1wey6f5Xapri8dMAVYuY \\
Theory Prop Id: & 4e94b5ab940a9c05d8ab92b169c0a80ff166d8866174805a6eccc7b684604233 \\
Theory Prop Address: & TMURjNJo39iyQq3Vy1vrzEGuvvAuAkto3iD
\end{tabular}
\end{center}

\end{theorem}
\section{explicit\_Field\_transfer}\label{fgihahmgjgdgjgehpfgejgfgmgegpfehchbgogdhggfgch}Let $ R : {\iota}$ be given.
Let $ zero one : {\iota}$ be given.
Let $ plus mult : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${plus}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${mult}$.
Let $ R' : {\iota}$ be given.
Let $ zero' one' : {\iota}$ be given.
Let $ plus' mult' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\infkdlckd$ as a right associative infix operator  corresponding to applying term ${plus'}$.
{\bf{Notation.}} We use $\infkdkckd$ as a right associative infix operator  corresponding to applying term ${mult'}$.
Let $ f : {{\iota}\unicdbdjdcd{\iota}}$ be given.
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfehchbgogdhggfgch} ${{{{{{{\mname{explicit\_Field}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}\unicdbdjdcd{{{{{\mname{bij}}~{R}}~{R'}}~{f}}\unicdbdjdcd{{{{f}~{zero}}={zero'}}\unicdbdjdcd{{{{f}~{one}}={one'}}\unicdbdjdcd{{({\unicdcdadad x y \in {R} .  {{{f}~{({{x}+{y}})}}={{{f}~{x}}\uniadadcdcg{{f}~{y}}}}})}\unicdbdjdcd{{({\unicdcdadad x y \in {R} .  {{{f}~{({{x}*{y}})}}={{{f}~{x}}\unicdbgcdgg{{f}~{y}}}}})}\unicdbdjdcd{{{{{{\mname{explicit\_Field}}~{R'}}~{zero'}}~{one'}}~{plus'}}~{mult'}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ef2cec44c7db17e7db32410fd90c52ba3fa20b7b18117cf540a99f8cbc44c289 \\
Pure Prop Address: & TMH4MjCpSyBbECQsWMxidZBXrRgD3jxBeiR \\
Theory Prop Id: & ac0144b31bec8f30802ed9e79cf8dd729ee2b3186952c3cb53f3e3d279b5d6e2 \\
Theory Prop Address: & TMHe1ubYe2eN5E7tR9x9YatesmwdpCoqbZC
\end{tabular}
\end{center}

\end{theorem}
\section{explicit\_Field\_RepIndep2}\label{fgihahmgjgdgjgehpfgejgfgmgegpfcffgahjeogegfgahcd}Let $ R : {\iota}$ be given.
Let $ zero one : {\iota}$ be given.
Let $ plus mult : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${plus}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${mult}$.
Let $ plus' mult' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\infkdlckd$ as a right associative infix operator  corresponding to applying term ${plus'}$.
{\bf{Notation.}} We use $\infkdkckd$ as a right associative infix operator  corresponding to applying term ${mult'}$.
Assume the following.
\begin{equation}
{\unicdcdadad a b \in {R} .  {{{a}+{b}}={{a}\uniadadcdcg{b}}}}\label{hyp:ieahahhc}
\end{equation}
Assume the following.
\begin{equation}
{\unicdcdadad a b \in {R} .  {{{a}*{b}}={{a}\unicdbgcdgg{b}}}}\label{hyp:iengnghc}
\end{equation}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfchfgahjgogegfgah} ${{{{{{{\mname{explicit\_Field}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}\unicdbdjded{{{{{{\mname{explicit\_Field}}~{R}}~{zero}}~{one}}~{plus'}}~{mult'}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 54840abeaa24e09c7beaa1936a5defc6c4ea07ae3fb67135a78d8477a50986cc \\
Pure Prop Address: & TMVPNiv37XT25SiNai41zYPSyiPfKQk6XPN \\
Theory Prop Id: & e0eee3acfed1c638458013101d378b56d17393576fd269927418992a1b7bcbc9 \\
Theory Prop Address: & TMRdcfuetQSDQ7zq6iYdygkjYWKXS2v6SE2
\end{tabular}
\end{center}

\end{theorem}
\section{Fields Encoded as Sets} % explicit_Field_RepIndep2
\begin{definition}\label{def:gejgfgmgeg}
We define $\mname{Field}$ to be ${\uniddcgcg F .  {{{\mname{struct\_b\_b\_e\_e}}~{F}}\unicdcdcdhd{{{\mname{unpack\_b\_b\_e\_e\_o}}~{F}}~{({\uniddcgcg Q plus mult zero one .  {{{{{{\mname{explicit\_Field}}~{Q}}~{zero}}~{one}}~{plus}}~{mult}}})}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & c7b84fda1101114e9994926a427c957f42f89ae1918086df069cb1a030519b46 \\
Pure Object Address: & TMaCGKsNBVewLEqMyTdCeiKd5uAgK8kFPjY \\
Theory Object Id: & 622c30c9ddf18abf87387ddef4f26b6be7b92f631ff5e6b4f5eabaac5839554b \\
Theory Object Address: & TMNqKgkVbs1Np95FXHhyjgcT3UAD21waXUL
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:gejgfgmgegpffhogahbgdglgpffgbh} ${\unicdcdadad R .  {\unicdcdadad plus mult : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {\unicdcdadad zero one .  {{{{\mname{unpack\_b\_b\_e\_e\_o}}~{({{{{{{\mname{pack\_b\_b\_e\_e}}~{R}}~{plus}}~{mult}}~{zero}}~{one}})}}~{({\uniddcgcg R plus mult zero one .  {{{{{{\mname{explicit\_Field}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}})}}={{{{{{\mname{explicit\_Field}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0da03c63995752d95dbfb4f0ee50676ef20f4ec29763384de9d7a7d83ec6a852 \\
Pure Prop Address: & TMG8uPxmuweznLRMtKvhzoTZwhtZUZ4zZ9d \\
Theory Prop Id: & 8e102fafcd372a62e72fe55218203e2c116e3761df378e4406f47cf88eb7c593 \\
Theory Prop Address: & TMbAKTnaoDqhKZZ3k6KRGTBNAbKxCGKqeLg
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfjgdhpfdecfjgoghgpfhhjgehigpfjgeg} ${\unicdcdadad F .  {{{\mname{Field}}~{F}}\unicdbdjdcd{{\mname{CRing\_with\_id}}~{F}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 26b551faed44acd5217dd94eab68e99a166869a3dfd0d404203d4386512d45c8 \\
Pure Prop Address: & TMH41wnx33D5QctmfmPNsPdyGr5hZzzsYVV \\
Theory Prop Id: & e3b51a97808ddcd82d668dd97352b7379f2a20e8f4731608e340953d0b7c4cf0 \\
Theory Prop Address: & TMQA24cveY5wc5Ys2Z97RVQgobE2zAHEJMR
\end{tabular}
\end{center}

\end{theorem}
\section{explicit\_OrderedField\_transfer}\label{fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfehchbgogdhggfgch}Let $ R : {\iota}$ be given.
Let $ zero one : {\iota}$ be given.
Let $ plus mult : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${plus}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${mult}$.
Let $ leq : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ be given.
{\bf{Notation.}} We use $\infmdnd$ as an infix operator  corresponding to applying term ${leq}$.
Let $ R' : {\iota}$ be given.
Let $ zero' one' : {\iota}$ be given.
Let $ plus' mult' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\infkdlckd$ as a right associative infix operator  corresponding to applying term ${plus'}$.
{\bf{Notation.}} We use $\infkdkckd$ as a right associative infix operator  corresponding to applying term ${mult'}$.
Let $ leq' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ be given.
Let $ f : {{\iota}\unicdbdjdcd{\iota}}$ be given.
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfehchbgogdhggfgch} ${{{{{{{{\mname{explicit\_OrderedField}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}\unicdbdjdcd{{{{{\mname{bij}}~{R}}~{R'}}~{f}}\unicdbdjdcd{{{{f}~{zero}}={zero'}}\unicdbdjdcd{{{{f}~{one}}={one'}}\unicdbdjdcd{{({\unicdcdadad x y \in {R} .  {{{f}~{({{x}+{y}})}}={{{f}~{x}}\uniadadcdcg{{f}~{y}}}}})}\unicdbdjdcd{{({\unicdcdadad x y \in {R} .  {{{f}~{({{x}*{y}})}}={{{f}~{x}}\unicdbgcdgg{{f}~{y}}}}})}\unicdbdjdcd{{({\unicdcdadad x y \in {R} .  {{{x}\unicdcdgded{y}}\unicdbdjded{{{leq'}~{({{f}~{x}})}}~{({{f}~{y}})}}}})}\unicdbdjdcd{{{{{{{\mname{explicit\_OrderedField}}~{R'}}~{zero'}}~{one'}}~{plus'}}~{mult'}}~{leq'}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d8a397eb2d41fc3df32161a85d5f88f8e1a1f828c3996623964e0cef70186f61 \\
Pure Prop Address: & TMPpLE4XGZTmn26HRXT5ka3vz3Konq3gJec \\
Theory Prop Id: & 5e1306d3daaaa9e52a4c86d25354e58525141369b79522baa7699df2d0fe77ea \\
Theory Prop Address: & TMau3sL5KTvBtt4AUk19sXEx1vw2u1rpj2V
\end{tabular}
\end{center}

\end{theorem}
\section{Selectors for Fields} % explicit_OrderedField_transfer
\begin{definition}\label{def:gejgfgmgegpfdgbgchchjgfgch}
We define $\mname{Field\_carrier}$ to be ${\uniddcgcg Fs .  {{Fs}~{0}}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & f0bb69e74123475b6ecce64430b539b64548b0b148267ea6c512e65545a391a1 \\
Pure Object Address: & TMY8sbcPiVs9VL311KPHpbm67U6sLM9JvF7 \\
Theory Object Id: & 9211e41eaf81bb8c152618cbe35230be60d736fcd5684c0b7bdc5ccc1ff70181 \\
Theory Object Address: & TMZQE6tPrFvJMaBcLrcMn85ZgscSeFbm4pT
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:gejgfgmgegpfahmgfhdh}
We define $\mname{Field\_plus}$ to be ${\uniddcgcg Fs .  {{\mname{decode\_b}}~{({{Fs}~{1}})}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 6968cd9ba47369f21e6e4d576648c6317ed74b303c8a2ac9e3d5e8bc91a68d9d \\
Pure Object Address: & TMYTM1QQGqgVyRM9unR8CLL2scwRHYvV3c3 \\
Theory Object Id: & ed06aa34b4112f8507370b46c1c5c7de7f2f9af4f24b831d45893ad3066e994e \\
Theory Object Address: & TMRiY7KU6BpU28KD19iwgBDLsQ5XyfpcbYL
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:gejgfgmgegpfngfhmgeh}
We define $\mname{Field\_mult}$ to be ${\uniddcgcg Fs .  {{\mname{decode\_b}}~{({{Fs}~{2}})}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 4b4b94d59128dfa2798a2e72c886a5edf4dbd4d9b9693c1c6dea5a401c53aec4 \\
Pure Object Address: & TMQSTL5b71ddbjnkjnGXfRZ61uXWmMGwJHD \\
Theory Object Id: & 7eb39ed695c795e4451a9252d011d377d0f4bdf0bfe6193f7a31ceb58f687a40 \\
Theory Object Address: & TMaJmzoi8UnDNTAXrAvZxYbTeEdKV3viygg
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:gejgfgmgegpfkhfgchpg}
We define $\mname{Field\_zero}$ to be ${\uniddcgcg Fs .  {{Fs}~{3}}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 61f7303354950fd70e647b19c486634dc22d7df65a28d1d6893007701d7b3df4 \\
Pure Object Address: & TMJzMmYjL1HdXDWMSRf7c775tmGDc6osaRL \\
Theory Object Id: & b74fb66a398c6c647d135ea9283353963f66d301d2c1ee126b203679f2071094 \\
Theory Object Address: & TMHQo21kvxiD8yab3ek4ATBz2PBfwvqsmaJ
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:gejgfgmgegpfpgogfg}
We define $\mname{Field\_one}$ to be ${\uniddcgcg Fs .  {{Fs}~{4}}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 57e734ae32adddc1f13e75e7bab22241e5d2c12955ae233ee90f53818028312a \\
Pure Object Address: & TMV8UDBZRqv4jocV6zt17aP89PcYugzQkoU \\
Theory Object Id: & b2fa78f7f58b95f4bc4f46ac268c3a959090897e56338c64bd84a73bc5fc2551 \\
Theory Object Address: & TMWFb9uZk2JEesS9quTe9a6Ww4ND9VcbBJA
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:gejgfgmgegpfngjgogfhdh}
$\mname{Field\_minus}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 9072a08b056e30edab702a9b7c29162af6170c517da489a9b3eab1a982fdb325 \\
Pure Object Address: & TMSqYJKBR2z1AqDFGucgVbSMyDGaQ2vHXdt \\
Theory Object Id: & 15e172a9ace52b84fbc8c26210b492b9383ddf56708a72b2b40566b8848bddcf \\
Theory Object Address: & TMN39qFAba46WDLPG5mn6arc4RJWRpLYRxY
\end{tabular}
\end{center}

\end{definition}
\section{Field}\label{gejgfgmgeg}Let $ Fs : {\iota}$ be given.
Assume the following.
\begin{equation}
{{\mname{Field}}~{Fs}}\label{hyp:iegedh}
\end{equation}
Let $F : {\iota}$ be ${{\mname{Field\_carrier}}~{Fs}}$.
Let $zero : {\iota}$ be ${{\mname{Field\_zero}}~{Fs}}$.
Let $one : {\iota}$ be ${{\mname{Field\_one}}~{Fs}}$.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${{\mname{Field\_plus}}~{Fs}}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${{\mname{Field\_mult}}~{Fs}}$.
{\bf{Notation.}} We use $\prenc{-}$ as a prefix operator  corresponding to applying term ${{\mname{Field\_minus}}~{Fs}}$.
\begin{theorem}\label{thm:gejgfgmgegpffgehbg} ${{Fs}={{{{{{\mname{pack\_b\_b\_e\_e}}~{F}}~{({{\mname{Field\_plus}}~{Fs}})}}~{({{\mname{Field\_mult}}~{Fs}})}}~{zero}}~{one}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d8b340ddeffe429e1fbbc93f3ec159869e95202bb0548fa01ab79999624db595 \\
Pure Prop Address: & TMcWSufBdeKRFXPYdLCveXwHxkWQ1G8Ku3s \\
Theory Prop Id: & 9308bd595b390a905ea8a71bb9251cf9b4ee7546ed5158a721de4d6eec1991fd \\
Theory Prop Address: & TMHvjr39A4G916GqBKMAajZKdrtBFnoqgcY
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpffgihahmgjgdgjgehpfgejgfgmgeg} ${{{{{{\mname{explicit\_Field}}~{F}}~{zero}}~{one}}~{({{\mname{Field\_plus}}~{Fs}})}}~{({{\mname{Field\_mult}}~{Fs}})}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 63dbf45fdb4fede703bd1ce1ee23508eef7fbbd8640d566b8ed583677d390af1 \\
Pure Prop Address: & TMYH7ErtGiAdfW9CrDDJ623kNniytKGVcjx \\
Theory Prop Id: & cb57dbd436ae765672438d8ff24477520b196a981db8feb13f2698511c06c6f2 \\
Theory Prop Address: & TMLZFScv2FGGQMRvkH7kAbY42toRcVj4bqQ
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfkhfgchpgpfjeog} ${{zero} \in {F}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5d2a12ae03ea09b1b00364de5be96f9417eba1807387eef0593c4686271f8b43 \\
Pure Prop Address: & TMV5NCa6Wx7gnzRhWo5AeVT8cTwstJid2DP \\
Theory Prop Id: & 124d417e36ffc4ecd962d65565094a8b6a908ebccf5fab90ad3c52962d4c8899 \\
Theory Prop Address: & TMJTmqQWrFwKLaFx3qyrzQjDtPmc6sNEAEL
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfpgogfgpfjeog} ${{one} \in {F}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 44022c6821b37c9bd64d3412ecf0090eea66e80eebb2def47c0ea8452f269ff2 \\
Pure Prop Address: & TMNtPhTBrbXJwXqr9MRjQjBCeakFLxdm4rA \\
Theory Prop Id: & 54c548fa567255c0074c7815ff32044eca656b312bcbb87e75ab72ac4e037c4c \\
Theory Prop Address: & TMaxye1k4K8yC8XLPLqCw4nFNFVXQMfGNmy
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfahmgfhdhpfdgmgpgdh} ${\unicdcdadad x y \in {F} .  {{{x}+{y}} \in {F}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6cb9ab847c2ae424b9e4a853861f83b1519ca940a43ca706c3f58543aa68e6f8 \\
Pure Prop Address: & TMSL8rTfsH4EGhTbnt4mmV2f3XC1kRDSuhc \\
Theory Prop Id: & 1404ed2bc6fc9cb6d24916d53178afcbbae9052d74dbddd08abb219ef3cc6988 \\
Theory Prop Address: & TMU5Koik3TBZQ4TJ7EcUGYpqbJxJUvF15eS
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngfhmgehpfdgmgpgdh} ${\unicdcdadad x y \in {F} .  {{{x}*{y}} \in {F}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 90491b3584ca5d345c64ad706ac87ca12bdae4cf2f13a8b47ed70d427919cb6a \\
Pure Prop Address: & TMXeFVMheHpzd5M1At9SBCuvJfvr5e1F4vX \\
Theory Prop Id: & 865f20b7a4b6f98b4c54586f84b21600d7e07243207713b57fa40e2ec5eda5ff \\
Theory Prop Address: & TMLt6bowMxotb2XT7CkV7ag3q8KNznCkvSg
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfahmgfhdhpfbgdhdhpgdg} ${\unicdcdadad x y z \in {F} .  {{{x}+{({{y}+{z}})}}={{({{x}+{y}})}+{z}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 49e71c4d43cf0fdaf6727db033c4e9e44f74cc50c7f11e8f287078c9de4186d6 \\
Pure Prop Address: & TMctJ6QSciEPYRwyuAGW91t49FWX5iwGskB \\
Theory Prop Id: & 5dac6c802dc58a4009410054756eb7533311da03f206d571ca13b54b7de62f48 \\
Theory Prop Address: & TMF9ZdDcMZBL4YbPNXREiZ4z6Ej4bQZGiAt
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfahmgfhdhpfdgpgng} ${\unicdcdadad x y \in {F} .  {{{x}+{y}}={{y}+{x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3b445936b40abf6f0f573b3695af272cd8f98957cd9977a5b0ca3f6dadd52baf \\
Pure Prop Address: & TMcSdkyySZ2JMLtoyeiiuVnq14co8TxbPgp \\
Theory Prop Id: & 27a761d026aec44ac48a86b672c56e46b77dfbf7622acf1151a03c5a486af018 \\
Theory Prop Address: & TMM9QF6dQ6HnJnFroaJHaH635ak1Jn8Jx1o
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfkhfgchpgpfme} ${\unicdcdadad x \in {F} .  {{{zero}+{x}}={x}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e0daa0e57cb9935241117668f353fd724bcb6173088571de6e8928a74ded74c9 \\
Pure Prop Address: & TMTonQi48JamuRgckkERNUD5uLVijoYmgL3 \\
Theory Prop Id: & 37d0579521bcd82e296de371d607f6dbe718d874c53486483fbe1d86059ae1e2 \\
Theory Prop Address: & TMUpYjiRJxYVxfan4X4iVYUVm3AfpaMR9Tf
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfahmgfhdhpfjgoggh} ${\unicdcdadad x \in {F} .  {\unicdcdaddd y \in {F} .  {{{x}+{y}}={zero}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 919ce52a6adadf0cc8094ecbe60076ee5858155672dd27ab2180e7e6c7bbe1f6 \\
Pure Prop Address: & TMN39v7z6H2CoUPdUhfYEYjvy3Zw4eENYPq \\
Theory Prop Id: & 262504b07a3f4e1940e4234afa8b6cb0e82cce09ab141e4e0d8b9675a6e62edd \\
Theory Prop Address: & TMJdMzeW7T3rZffNfiYy8hAcNdvCNvWPow9
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngfhmgehpfbgdhdhpgdg} ${\unicdcdadad x y z \in {F} .  {{{x}*{({{y}*{z}})}}={{({{x}*{y}})}*{z}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 08143128b200fbed930f0fff6e90f4cb05098f19ae900fd1f1cb0beb563e2c09 \\
Pure Prop Address: & TMc9dXbETfWeBa2b8YnDKbhLw7uaVyQboHe \\
Theory Prop Id: & bad75ea2350024fa534d6b728d0eba5cf28e28fbe493d52077a0cc7bedc82c9d \\
Theory Prop Address: & TMLXQH9iTPeEeNTAWWLcpo5cJTA4AgEWJuq
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngfhmgehpfdgpgng} ${\unicdcdadad x y \in {F} .  {{{x}*{y}}={{y}*{x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b067a98764ad614c2eab7437092942718dbd9dd9a388f583ce6d32e68bd7dd64 \\
Pure Prop Address: & TMPegBnUirvhxDN9mWgopPcPibU15GBD2aT \\
Theory Prop Id: & 95c74fc682d34ffea07fca550e5dfd7573581c19dd74de76bca295caa9119383 \\
Theory Prop Address: & TMSy5iWokESs8xWZnGcamGMUMENTfP5k3Jh
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfpgogfgpfogfgbhpfkhfgchpg} ${{one}\unicdcdgdad{zero}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0cd6b9f7a2a8864851fc03b62eca322da80ca6a538426cf27bba6634e3656726 \\
Pure Prop Address: & TMbSs4K7qkmEkJCui8RQ5ucU6Bxp9AhXSiP \\
Theory Prop Id: & 266cd947601e72d416352cfdc17094f13320ebf353611367683f3cf2c946d097 \\
Theory Prop Address: & TMUvPmKRiKPF1BAM9e9AAYevwEYsUoNceXf
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfpgogfgpfme} ${\unicdcdadad x \in {F} .  {{{one}*{x}}={x}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f43915f1f2955af2eb66b15dad875d94d73d7b7b9834e7c9adb0f55df5881fe9 \\
Pure Prop Address: & TMXMDwpgqy9TopEv1E4DfdDaXfqz9tA6hLH \\
Theory Prop Id: & 013427804b41d47918f24b864b24aab70dfc31113ba98edcd33612349510178b \\
Theory Prop Address: & TMZ8XZoWUvugHdtZXDcG1tmeGAV5J4gRkxN
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngfhmgehpfjgogghpfme} ${\unicdcdadad x \in {F} .  {{{x}\unicdcdgdad{zero}}\unicdbdjdcd{\unicdcdaddd y \in {F} .  {{{x}*{y}}={one}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 159c70606656e548df27dc9f2989d005a799bc59dfc48530c9aaef4d88bfe55a \\
Pure Prop Address: & TMPGyXrYchHMpQoxBotw4fTsy9qkcod1cXb \\
Theory Prop Id: & 99224d179a2cb454d745622ccfd66d3d60660e4bde41c61da98aa4dd3e938ee4 \\
Theory Prop Address: & TMH8ZcNMHvhfoVar9hvT3VD2o3DW9jyeJdr
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfegjgdhehchpfme} ${\unicdcdadad x y z \in {F} .  {{{x}*{({{y}+{z}})}}={{{x}*{y}}+{{x}*{z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 250384aaa9ecf10fbcf4ebefa3dc489b41d3cb10f656500151d49a9053cfe4f9 \\
Pure Prop Address: & TMZiuCgz7mgpvcfSTTHjcdzaaeZFaZEUrv8 \\
Theory Prop Id: & 0ebf99ce21204a4f57fb5783b2803ac92906cc63624dd2cc67cc70a1353aeee0 \\
Theory Prop Address: & TMUjioKdcupXefDDTsQSWE2Vw19Nna8245U
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:gejgfgmgegpfegjggh}
$\mname{Field\_div}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 33f36e749d7a3683affaed574c634802fe501ef213c5ca5e7c8dc0153464ea3e \\
Pure Object Address: & TMR6i3AfWJEnAVs3vStqGHLoyVAtt7HuhVZ \\
Theory Object Id: & 3a617adfbc7761f4bff8c1a67cc5a2811928c372828b963f2809216d145f0056 \\
Theory Object Address: & TMKD8yCQcW3giMss49AdhftfjbmKvDhxqNd
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infkdpckd$ as an infix operator  corresponding to applying term ${\mname{Field\_div}}$.
\begin{theorem}\label{thm:gejgfgmgegpfegjgghpfahchpgah} ${\unicdcdadad x \in {F} .  {\unicdcdadad y \in {{F}\unicdcdbdgd{\{{zero}\}}} .  {{{{x}:/:{y}} \in {F}}\unicdcdcdhd{{x}={{y}*{({{x}:/:{y}})}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 320029a8925ea4f20053afa631f90353310f8bd2a02fc1312664ae3d5e617bab \\
Pure Prop Address: & TMLCRGM73NJSReYA8S8dFeUvsVHD5BezMmw \\
Theory Prop Id: & 11f8a74d8832813bb0bf2e47adbaecaec90b4bb4ffc2917b900e65c5fdfcd21a \\
Theory Prop Address: & TMFtSZaRxbLf7cg7s9eC7F24ERy3YpttcjS
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfegjgghpfdgmgpgdh} ${\unicdcdadad x \in {F} .  {\unicdcdadad y \in {{F}\unicdcdbdgd{\{{zero}\}}} .  {{{x}:/:{y}} \in {F}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ae15934f0050805acbad83a7ea9b08d39343e7275a2aa0544983f8c3029b68ab \\
Pure Prop Address: & TMLj2rQAk7mQRGGwfxY9ab6r8GZpdh5nryZ \\
Theory Prop Id: & f08d2cba3fd57f474e2e6a9ed26207be75354dfc72cde6a65408f169f301435a \\
Theory Prop Address: & TMLDYbyYNgVKinoxufwLvutrLNRfnk66vDt
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngfhmgehpfegjggh} ${\unicdcdadad x \in {F} .  {\unicdcdadad y \in {{F}\unicdcdbdgd{\{{zero}\}}} .  {{x}={{y}*{({{x}:/:{y}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1bda12fe605e6023cf81fa8393926be18b348502472ef7b4c757036a807eff68 \\
Pure Prop Address: & TMb6WJncGKrL2byhXB2YuUpprymEHFctWHV \\
Theory Prop Id: & c8ef92ac56a58978069a954b8be3acacbe73d63049ec632444d403ecbafb062b \\
Theory Prop Address: & TMEsHD4dd1bPW6M8yUdXaW4UYoSXZQW37fk
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfegjgghpffhogegfgggbd} ${\unicdcdadad x y .  {{{x}\unicdcdadjd{F}}\unicdbdjdcd{{{x}:/:{y}}={0}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 20e2690180e6250c71da49027a7a363d806e4fdad713709dbf99337aaa83d216 \\
Pure Prop Address: & TMWhJ43K252biCbrmZvzzeVwqqpjcQVZBxU \\
Theory Prop Id: & b5ccab25818eb5893b4528f4adc070775587f1a1b252b703a355452ef3ec25ef \\
Theory Prop Address: & TMS9ggt9Tn8AYLjGKxejwDFj1op6j9f7TWs
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfegjgghpffhogegfgggcd} ${\unicdcdadad x y .  {{{y}\unicdcdadjd{F}}\unicdbdjdcd{{{x}:/:{y}}={0}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 08ea037ff82421470289f5932634b1ce136fcb6d1f8706fa6883561e9bff8d34 \\
Pure Prop Address: & TMUWRvAmiES3iybNvXn7sUoxZwKmagyQ8rC \\
Theory Prop Id: & 6c03f1015d94454404a03499287892345ea00012a20efb26d3b80fcf490734cd \\
Theory Prop Address: & TMLn5yRrKaaMpTjWyKDfNinNPu78LWX738s
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfegjgghpffhogegfgggdd} ${\unicdcdadad x .  {{{x}:/:{zero}}={0}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5c48b82d4fc362fe344e205c36ca6878bd5138f2eb8555efdd2826a31ede70e2 \\
Pure Prop Address: & TMcjdraN7C77qSyG5w9GJM3oWt4kL3HUmCG \\
Theory Prop Id: & 24e90d5e4e5f1d4012652a7c973b6fdadb4b7a94e33c52e4c0945440a41f612e \\
Theory Prop Address: & TMUNnuEej7hLE5MrRKfW9mQkKWFqHyvwbkp
\end{tabular}
\end{center}

\end{theorem}
{\bf{Notation.}} We use $\infof$ as a right associative infix operator  corresponding to applying term ${{\mname{CRing\_with\_id\_omega\_exp}}~{Fs}}$.
\begin{theorem}\label{thm:gejgfgmgegpfpgngfghgbgpffgihahpfad} ${\unicdcdadad x .  {{{x}^{0}}={one}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4362c28e2db5e3383addcc627e5b9fc5c9d8d6e0b00cb0d2216109cbb0b3cfb0 \\
Pure Prop Address: & TMNwr244Poo2trbPpcVQmtxpagskYic6goM \\
Theory Prop Id: & 4527b98489253d272cf17c4b7c4e4690a8ebdb756ee228c39e35e2396e350909 \\
Theory Prop Address: & TMKmcrh5e3aKCAfTomskajMoU8zcUuiFdRz
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfpgngfghgbgpffgihahpfdf} ${\unicdcdadad x .  {\unicdcdadad n \in {\mname{omega}} .  {{{x}^{({{\mname{ordsucc}}~{n}})}}={{x}*{{x}^{n}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d2e5103c06f38d501b5624ac09de58fe1199ed0428e0099e2cecd857b56c9463 \\
Pure Prop Address: & TMRxJHnciqiQFbYupzsqKnpymvXkgoFKbz2 \\
Theory Prop Id: & 414637f793aeaef595d4415aea905c8712dd128bdf3888d6a1b8b79c783f993f \\
Theory Prop Address: & TMXUtYW7Vcrt9RLnqAwfxxVBZXyfpj7hTyU
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfpgngfghgbgpffgihahpfbd} ${\unicdcdadad x \in {F} .  {{{x}^{1}}={x}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 351bec92d644d3d3f57736c30184720a55a3206dd32c5c5de668a1a15d21cf70 \\
Pure Prop Address: & TMKtTCkPJ5sHx3gK7y8wuSN5Rfkt5hunA6A \\
Theory Prop Id: & 97fa394baba04b04edef47f65fc4ec793503e5777b288b978d77b4c9bb64fe45 \\
Theory Prop Address: & TMTi7WjdmiDN2vrsRDu17s69nAUYnNDuowU
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfpgngfghgbgpffgihahpfdgmgpgdh} ${\unicdcdadad x \in {F} .  {\unicdcdadad n \in {\mname{omega}} .  {{{x}^{n}} \in {F}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 026ac1d1f5ef29832893f6c7944103acad2da742c648c31b129e3d067c5334f3 \\
Pure Prop Address: & TMSeptsHCdwBLhRoQhW2RzWACc5328SueZM \\
Theory Prop Id: & 8e8df3c69edbfdbdf46653edec4be7381ff02d8b6f0c54facfc9849a6b7ad1fb \\
Theory Prop Address: & TMJ98yveoAeohCchdDEX5eSGLgbMb5NtmQ4
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpffgghbgmgpfahpgmgjhpfdgmgpgdh} ${\unicdcdadad n \in {\mname{omega}} .  {\unicdcdadad cs \in {{F}^{{n}}} .  {\unicdcdadad x \in {F} .  {{{{{{\mname{CRing\_with\_id\_eval\_poly}}~{Fs}}~{n}}~{cs}}~{x}} \in {F}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 339c6079b932e105f62ee9a139090ec0c35d05a91b77324b7c9d00829f5e157a \\
Pure Prop Address: & TMUHU4Kdwck1DovJNNC1BznGxQ9LfqrpcD2 \\
Theory Prop Id: & e3e5a122a52cb88471f32d0108c8ebfd779225b3f222aaa00e6b00105eb91521 \\
Theory Prop Address: & TMWrCNHLicENtgPnEmebmghuFpCDVv9acP4
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfahmgfhdhpfdgbgogdgfgmgme} ${\unicdcdadad x y z \in {F} .  {{{{x}+{y}}={{x}+{z}}}\unicdbdjdcd{{y}={z}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 443b41e62519d1cf11ce79b28ce6902b1cb036b303feb0522d8233e77510b0da \\
Pure Prop Address: & TMQYEe7aS7C6puTrXwtgHP1HzLv6iA9FCYV \\
Theory Prop Id: & 65814d60a21e4514adfe8122a71e77983e1c014e2364364e2b428a8e889110d1 \\
Theory Prop Address: & TMPeQdMTjszQk8ZwjKbe2Yx9p1bhEuku2th
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfahmgfhdhpfdgbgogdgfgmgcf} ${\unicdcdadad x y z \in {F} .  {{{{x}+{z}}={{y}+{z}}}\unicdbdjdcd{{x}={y}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f16e614fd8bcca5468eff3f77a1ffdbdf61ce6894a9642616315fd8217fa6896 \\
Pure Prop Address: & TMHxcrqScEQVs2BM9LqdwdJ73QaGHTHjtAw \\
Theory Prop Id: & 5f414f4ccd4d5d42eb071a720d4cfd7f8e2a864a6d3ffecc438de4a083e92c4d \\
Theory Prop Address: & TMMUfLR9eAhuBx9dH38X5X7iGs36sxjomLw
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngjgogfhdhpffgbh} ${\unicdcdadad x \in {F} .  {{\prenc{{x}}}={{{{{{{\mname{explicit\_Field\_minus}}~{F}}~{zero}}~{one}}~{({{\mname{Field\_plus}}~{Fs}})}}~{({{\mname{Field\_mult}}~{Fs}})}}~{x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & de7b3a103710cd73b730d9ab58f9ad4f2d88bd767fec9ca2edba308880936b16 \\
Pure Prop Address: & TMVexy4tBFivo588m7GQ84C5mQBJ4yZx98Z \\
Theory Prop Id: & f6684a8b3c3ff9441214e19ef1db049db0227f25e3db1d329cfd06250e47f513 \\
Theory Prop Address: & TMGtBPcXh4HJHkfMAC1yckyY5RPTB4NACYW
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngjgogfhdhpffhogegfggg} ${\unicdcdadad x .  {{{x}\unicdcdadjd{F}}\unicdbdjdcd{{\prenc{{x}}}={0}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 357d777053f15331bc00d78b8e12f89dc8130cc8c44f2c6131dcc55defa8ee0f \\
Pure Prop Address: & TMTwnPHTSFHEiMGLciYU9XDmEYP1U9Z2eZN \\
Theory Prop Id: & 60ed459a7799cd3e857363ae83693d0f4826d792577f17db36e25c07793bc296 \\
Theory Prop Address: & TMW6cjVsvwBeiH3JX9mV7y27yXLNaXoLkjr
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngjgogfhdhpfdgmgpgdh} ${\unicdcdadad x \in {F} .  {{\prenc{{x}}} \in {F}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f1becfbfee0ef8b26de040c7f18230ec7527ddcf884ada3c8941b9b5c6de9b87 \\
Pure Prop Address: & TMbwyWNKrfuYFG1TmqXNEzZJ4rHSH3Yvzwv \\
Theory Prop Id: & d590d7bb3e9f5cb4915a63f72350aaa482789cd650f74ceaa143f1b01be467b9 \\
Theory Prop Address: & TMKy1fXBQm9Ci94udEjidssK8Da4zqwq6BX
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngjgogfhdhpfcf} ${\unicdcdadad x \in {F} .  {{{x}+{\prenc{{x}}}}={zero}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5cb54808b5cc0bfe1a9faf501b5e357f53bff36ec590e8f602fed76ba642d4b3 \\
Pure Prop Address: & TMR6vs3rpH6qDTpNibPSbTftrd3h5nzUygq \\
Theory Prop Id: & 2391ef531b49ac2b610cb94e6726c81909131c9e4acf4d3aa6ee03f5bdeea688 \\
Theory Prop Address: & TMMcagzy7PNZ6o6f6y6gxJVCHKFabzvbY1n
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngjgogfhdhpfme} ${\unicdcdadad x \in {F} .  {{{\prenc{{x}}}+{x}}={zero}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7c66759f9e4abb07e2159e5e1557c1602f8cb0f7f38d7aeae89ee98bbc859ebe \\
Pure Prop Address: & TMHN25GQoh4jYakdvcZYx96QdJXH514To2u \\
Theory Prop Id: & b5cf76ad592ab4b5a7384338d4297cf97c6981dd0a45ac579115230625384cc5 \\
Theory Prop Address: & TMXuvPZ1qizoaTqpK2wbJgJGEjrtducR28f
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngjgogfhdhpfjgogghpgmg} ${\unicdcdadad x \in {F} .  {{\prenc{{\prenc{{x}}}}}={x}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e097d2ad2fa0d0d1bf0193b8e412f65b42e3e5c73733c262d1b7eeb1cbd57883 \\
Pure Prop Address: & TMMMeGBCnj2s3dzeT7Yfa9bpUfU46psmpSe \\
Theory Prop Id: & 7f6c7d184b0f20e8f912398c740d072ae44f16dc17d5358d415b7f2a5ccdece3 \\
Theory Prop Address: & TMTzNG5pZe3QRegKNVBSsZp3PqJjsutAt1f
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngjgogfhdhpfpgogfgpfjeog} ${{\prenc{{one}}} \in {F}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fbd93d93f1671451fec2d592c753cd960b2e1288c4241e1fad9a57ee7a022c02 \\
Pure Prop Address: & TMHWKgvtYjVJyEYbaQY7sTTe4usgtgVj9LS \\
Theory Prop Id: & 61a82a30b97b7f4fb97d4f6625d6e919a0010537baceadb9f9b571c21d50a9f8 \\
Theory Prop Address: & TMSwuqi7dSFVmvwt5crCA1gi7nDJn439QVp
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfkhfgchpgpfngfhmgehcf} ${\unicdcdadad x \in {F} .  {{{x}*{zero}}={zero}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 45513e8074cff3c93f264cf92510bcaed6b453af70ec391191356622b3682292 \\
Pure Prop Address: & TMPYu6VMYJksB1pVtcZhxA1ZtBtBiyAQA3q \\
Theory Prop Id: & fadc07fc14b79ffe08eb28c7b3dd0a9607e542c43123389eacca8922d9a3bbd6 \\
Theory Prop Address: & TMWgQLa4SJqx34swEHxJoxG1BrHPgR8ESyy
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfkhfgchpgpfngfhmgehme} ${\unicdcdadad x \in {F} .  {{{zero}*{x}}={zero}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5ee5eb5fde0181d92b2c7f6d7a2a896cd74e3a750cdabbb27d94b1bb4aab908c \\
Pure Prop Address: & TMLc5uhw7hxR8sbQGdBpQkCtjeGhbq6hy1L \\
Theory Prop Id: & 3e7854299ba2aa2daea10889a8309962f1b1d6c32b7006fc1c40500925221173 \\
Theory Prop Address: & TMRcY5cpYprw5iQzhQcoGB6ndppCPbrhUtT
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngjgogfhdhpfngfhmgeh} ${\unicdcdadad x \in {F} .  {{\prenc{{x}}}={{({\prenc{{one}}})}*{x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7cd676e4adffa30d0cf22cf26fcde8bfd203a61ee59f416b12fa62cfd93db1b7 \\
Pure Prop Address: & TMHF8RJu8ok4xK5Js75hyF7aTwTeYUktaWC \\
Theory Prop Id: & 775b246ad68e751222cbcb9a5e49e184ed3019fcce6a74f91edd30125e3f0098 \\
Theory Prop Address: & TMQzhW2ohogP8qPJxruSSb4HgNFe1kHyJaE
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngjgogfhdhpfpgogfgpfdhbhfhbgchfg} ${{{({\prenc{{one}}})}*{({\prenc{{one}}})}}={one}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f1d40df6baeeb2bbfbb7f411d9caeb48477cc6718458d7e70ca7bd1b7a78d1cc \\
Pure Prop Address: & TMPY9Fe2gL8ytA1WVeKrmqRrbe6bXkndVWA \\
Theory Prop Id: & 4f370c1adbdb484572d2f537b4a62640f4e6192dcbbfc4d7dee46fb09f3433e6 \\
Theory Prop Address: & TMYd1s86jR7deZ3QCmxu2FzfXcVu8tMBNyU
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngjgogfhdhpfdhbhfhbgchfg} ${\unicdcdadad x \in {F} .  {{{({\prenc{{x}}})}*{({\prenc{{x}}})}}={{x}*{x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a55d0e9b98e66f6d5322b6523e3e708815bb201d618aa58f328931f5f07d0f37 \\
Pure Prop Address: & TMN6DCGTRZLbdyYaDBJ9hD7em3K6sLzKydd \\
Theory Prop Id: & 726593b03eefe34d9157a17b6e679b85bcf1865e151930e64fe462ee18a8a6a9 \\
Theory Prop Address: & TMNpHhjMNCtccTVy7oxGE8LEDQS3ikFDxRL
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngjgogfhdhpfkhfgchpg} ${{\prenc{{zero}}}={zero}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f5214a9560f5568380d8be3826be07444fe57c851dd66aa09a5764efb8077718 \\
Pure Prop Address: & TMNcsvycuD4vkz4pfqQk1YGD8DMTSNJU4AH \\
Theory Prop Id: & 25e6829a5bf06f2eaecafec005fea75bb87bdbfe0e161ec9b16912fa023dc76d \\
Theory Prop Address: & TMXQJxi91EWkUHXgdLamfSNazD2x5oL6iHv
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfegjgdhehpfcf} ${\unicdcdadad x y z \in {F} .  {{{({{x}+{y}})}*{z}}={{{x}*{z}}+{{y}*{z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & deb7136831fde91f8aaab03eb0c31cdcadb1e244807de445094801e21f93cc47 \\
Pure Prop Address: & TMdNLPJWkse1Z9urNENt7q5Qeyf5LwWd49a \\
Theory Prop Id: & 10fe6a61397ce15f1f074447b70bfba8150ab8b2d77f7129a3ca0d5dda084ce2 \\
Theory Prop Address: & TMNDDzYVTXFEChN6smH4YbceCPCtL4pBEz9
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngjgogfhdhpfahmgfhdhpfegjgdheh} ${\unicdcdadad x y \in {F} .  {{\prenc{{({{x}+{y}})}}}={{\prenc{{x}}}+{\prenc{{y}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7d70513a02d66f0f56d24e5c8cab215e006349e8a3dbcd5fd887d9d1dcc56fe1 \\
Pure Prop Address: & TMKE1EAuG9tUBJEqHNho1ojpdVMUyyVrRkp \\
Theory Prop Id: & cf09f8db6ef5dbb5d2ed9a9695a44c7323061de997ed2f25e7785eb1d93e4486 \\
Theory Prop Address: & TMRjUdfwmx5YiiXEHvkgNMeZ615jeu3ixtf
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngjgogfhdhpfngfhmgehpfme} ${\unicdcdadad x y \in {F} .  {{{({\prenc{{x}}})}*{y}}={\prenc{{({{x}*{y}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 58520e0833b7099a6940ba9408893dd9df17b42fbcadaeb89d0b3be3b1d4b459 \\
Pure Prop Address: & TMF5FPzDp822hueufQ3yiZiRPZucSMkbB1N \\
Theory Prop Id: & 09040b49c949f9afb231e21ee54bb76add27e0f1944d83e5dfdea037fb2b5e78 \\
Theory Prop Address: & TMHvcKKRtR69YcV7eYTB3batvpaofCBGg4b
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngjgogfhdhpfngfhmgehpfcf} ${\unicdcdadad x y \in {F} .  {{{x}*{({\prenc{{y}}})}}={\prenc{{({{x}*{y}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0f87ffe9baf0ac37844ca25d819bbf2e6b56af4a7acba178604fef6b2c73975b \\
Pure Prop Address: & TMNFhiGH735rxLAYHzqXjLVSVhiSUKYVJFj \\
Theory Prop Id: & d3e4735bbc06ae8a25cb40640c44781c9e83add0c02c7c02058ad54bddb5536e \\
Theory Prop Address: & TMbXkVYiquoTVr7qFbrQXZCThaRMHyD72Na
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfdhbhfhbgchfgpfkhfgchpgpfjgoggh} ${\unicdcdadad x \in {F} .  {{{{x}*{x}}={zero}}\unicdbdjdcd{{x}={zero}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2b2bd6de108abc8d3794de6a31f5341040d00d973de79329c574098caed59e31 \\
Pure Prop Address: & TMZKCqVzNkAqM9J9D53Y9aBiDZvqkPQkdVB \\
Theory Prop Id: & 08c2f8793e760cef2edbc292e690c746158bd7259df3295852d68c7214236e65 \\
Theory Prop Address: & TMUCadVDmPtHtGW9E9rogNfiQCpPtyuh4MU
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfngfhmgehpfkhfgchpgpfjgoggh} ${\unicdcdadad x y \in {F} .  {{{{x}*{y}}={zero}}\unicdbdjdcd{{{x}={zero}}\unicdcdcdid{{y}={zero}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e191e1698c04a863c4f10266ada28dbd2db7490864c6c1c80f7dc9b6049a62ab \\
Pure Prop Address: & TMY8AV6XaQZR4ezqWu2BT6WM441CDJBthsX \\
Theory Prop Id: & fbeb3acafb828d177072b74d6982e4e3a3df773c746d4ea7168c3a03b93613bd \\
Theory Prop Address: & TMYaR1LATsRePnNzvKfW1CMi8VJXyAhwf3e
\end{tabular}
\end{center}

\end{theorem}
\section{Field2}\label{gejgfgmgegcd}Let $ Fs : {\iota}$ be given.
Let $ Fs' : {\iota}$ be given.
Let $F : {\iota}$ be ${{\mname{Field\_carrier}}~{Fs}}$.
Let $zero : {\iota}$ be ${{\mname{Field\_zero}}~{Fs}}$.
Let $one : {\iota}$ be ${{\mname{Field\_one}}~{Fs}}$.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${{\mname{Field\_plus}}~{Fs}}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${{\mname{Field\_mult}}~{Fs}}$.
Let $F' : {\iota}$ be ${{\mname{Field\_carrier}}~{Fs'}}$.
Let $zero' : {\iota}$ be ${{\mname{Field\_zero}}~{Fs'}}$.
Let $one' : {\iota}$ be ${{\mname{Field\_one}}~{Fs'}}$.
{\bf{Notation.}} We use $\infkdlckd$ as a right associative infix operator  corresponding to applying term ${{\mname{Field\_plus}}~{Fs'}}$.
{\bf{Notation.}} We use $\infkdkckd$ as a right associative infix operator  corresponding to applying term ${{\mname{Field\_mult}}~{Fs'}}$.
{\bf{Notation.}} We use $\prenc{-}$ as a prefix operator  corresponding to applying term ${{\mname{Field\_minus}}~{Fs}}$.
{\bf{Notation.}} We use $\prekdnckd{-}$ as a prefix operator  corresponding to applying term ${{\mname{Field\_minus}}~{Fs'}}$.
\begin{definition}\label{def:dhfhcgggjgfgmgeg}
$\mname{subfield}$ is the opaque object of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 9216abdc1fcc466f5af2b17824d279c6b333449b4f283df271151525ba7c9aca \\
Pure Object Address: & TMJhV7ybK4sNoy7dLu16XHkQMMh2u7ogDg9 \\
Theory Object Id: & 8b767b8278051b976eaa45775446a5c3d3fb3b6c01e0d6652741dd499114ae43 \\
Theory Object Address: & TMGfnnZhzcvAyc6uD3itbd4JQrSmEALeWf1
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:dhfhcgggjgfgmgegpfje} ${{{\mname{Field}}~{Fs}}\unicdbdjdcd{{{\mname{Field}}~{Fs'}}\unicdbdjdcd{{{F} \subseteq {F'}}\unicdbdjdcd{{{zero}={zero'}}\unicdbdjdcd{{{one}={one'}}\unicdbdjdcd{{({\unicdcdadad a b \in {F} .  {{{a}+{b}}={{a}\uniadadcdcg{b}}}})}\unicdbdjdcd{{({\unicdcdadad a b \in {F} .  {{{a}*{b}}={{a}\unicdbgcdgg{b}}}})}\unicdbdjdcd{\mname{subfield}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7e727ad2e5128678d00eab2e3f41718c941d248ab8bc80d9290e8e449722a6cf \\
Pure Prop Address: & TMM7f9u7WrEFj8YHR1zoL7g1oxSnnpx4nuA \\
Theory Prop Id: & d7fa7daaa1fd31a6790debe2a61072593e062f53926bea2d384140301fd0f3c5 \\
Theory Prop Address: & TMTAZrzxHvVF3ivGCdEm8NHia2yU7XfKPxD
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dhfhcgggjgfgmgegpffe} ${{\mname{subfield}}\unicdbdjdcd{\unicdcdadad p : {o} .  {{({{{\mname{Field}}~{Fs}}\unicdbdjdcd{{{\mname{Field}}~{Fs'}}\unicdbdjdcd{{{F} \subseteq {F'}}\unicdbdjdcd{{{zero}={zero'}}\unicdbdjdcd{{{one}={one'}}\unicdbdjdcd{{({\unicdcdadad a b \in {F} .  {{{a}+{b}}={{a}\uniadadcdcg{b}}}})}\unicdbdjdcd{{({\unicdcdadad a b \in {F} .  {{{a}*{b}}={{a}\unicdbgcdgg{b}}}})}\unicdbdjdcd{p}}}}}}}})}\unicdbdjdcd{p}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d7e94964874d4552f7612152bc7b4fe8077a730735f362aadb7346233bbbc7eb \\
Pure Prop Address: & TMTNHkoYxk53iGUuEwSw3EVWoAuX1WUvdw8 \\
Theory Prop Id: & e75e56a8a51307bd8de2cf55f809fee0d2458291f278ceed9218a3d441845a43 \\
Theory Prop Address: & TMNqv7RamAPGivDz6Nh19aHNfkFEMuvESP4
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:gejgfgmgegpfiepgng}
$\mname{Field\_Hom}$ is the opaque object of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 597c2157fb6463f8c1c7affb6f14328b44b57967ce9dff5ef3c600772504b9de \\
Pure Object Address: & TMGp1283AAzgHauWyMFM6fwpTKhT2UvW44v \\
Theory Object Id: & 30bf3301fb81b8870c663685fc6bfa8593d92c4bb8d8baedadeac04223d7577b \\
Theory Object Address: & TML6Zjm746Vd3N4sjVSwnNb4J5yLWD6e5Yj
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:gejgfgmgegpfiepgngpfje} ${\unicdcdadad g .  {{{\mname{Field}}~{Fs}}\unicdbdjdcd{{{\mname{Field}}~{Fs'}}\unicdbdjdcd{{{g} \in {{F'}^{{F}}}}\unicdbdjdcd{{{{g}~{zero}}={zero'}}\unicdbdjdcd{{{{g}~{one}}={one'}}\unicdbdjdcd{{({\unicdcdadad a b \in {F} .  {{{g}~{({{a}+{b}})}}={{{g}~{a}}\uniadadcdcg{{g}~{b}}}}})}\unicdbdjdcd{{({\unicdcdadad a b \in {F} .  {{{g}~{({{a}*{b}})}}={{{g}~{a}}\unicdbgcdgg{{g}~{b}}}}})}\unicdbdjdcd{{\mname{Field\_Hom}}~{g}}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 31c68d4d1908803e35c198b4917b363aece27f736abc525d3be26b2bbfaf25ed \\
Pure Prop Address: & TML1nC9DaTHq5nADe4PBSDz3pRDBKuM4coa \\
Theory Prop Id: & 12959a75af826745c76c8cacac56b223b08b5dfa4b785d1f4dbe42ad5c2234c4 \\
Theory Prop Address: & TMFvSuVBfh1siZrHxBxDNdzASV8SPhqhWGz
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfiepgngpffe} ${\unicdcdadad g .  {{{\mname{Field\_Hom}}~{g}}\unicdbdjdcd{\unicdcdadad p : {o} .  {{({{{\mname{Field}}~{Fs}}\unicdbdjdcd{{{\mname{Field}}~{Fs'}}\unicdbdjdcd{{{g} \in {{F'}^{{F}}}}\unicdbdjdcd{{{{g}~{zero}}={zero'}}\unicdbdjdcd{{{{g}~{one}}={one'}}\unicdbdjdcd{{({\unicdcdadad a b \in {F} .  {{{g}~{({{a}+{b}})}}={{{g}~{a}}\uniadadcdcg{{g}~{b}}}}})}\unicdbdjdcd{{({\unicdcdadad a b \in {F} .  {{{g}~{({{a}*{b}})}}={{{g}~{a}}\unicdbgcdgg{{g}~{b}}}}})}\unicdbdjdcd{{({\unicdcdadad a \in {F} .  {{{g}~{({\prenc{{a}}})}}={\prekdnckd{{{g}~{a}}}}}})}\unicdbdjdcd{{({\unicdcdadad a \in {F} .  {{{{g}~{a}}={zero'}}\unicdbdjdcd{{a}={zero}}}})}\unicdbdjdcd{{({\unicdcdadad a b \in {F} .  {{{{g}~{a}}={{g}~{b}}}\unicdbdjdcd{{a}={b}}}})}\unicdbdjdcd{{({\unicdcdadad a \in {F} .  {\unicdcdadad n \in {\mname{omega}} .  {{{g}~{({{{{\mname{CRing\_with\_id\_omega\_exp}}~{Fs}}~{a}}~{n}})}}={{{{\mname{CRing\_with\_id\_omega\_exp}}~{Fs'}}~{({{g}~{a}})}}~{n}}}}})}\unicdbdjdcd{p}}}}}}}}}}}})}\unicdbdjdcd{p}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0ba6afb6588f84ed9233205763416bbcb48104160ae81e7c83aaa749df56f30a \\
Pure Prop Address: & TMHyWBfPWgBD8fHLFmj2uHd8LiGwzKaPXbL \\
Theory Prop Id: & 4bd91ea8df1144675fc91986c05fe9c6aa39bb2352629ee956d785fb210304d0 \\
Theory Prop Address: & TMd7scvhecxt55fo9HQefDSbDkqviHLYMQk
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfiepgngpfjgogkg} ${\unicdcdadad g .  {{{\mname{Field\_Hom}}~{g}}\unicdbdjdcd{\unicdcdadad a b \in {F} .  {{{{g}~{a}}={{g}~{b}}}\unicdbdjdcd{{a}={b}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 68a0d1b5c80c7bc045dfade09ce3a0bf9500817cee9a0014553c03d27df85b25 \\
Pure Prop Address: & TMb9HZYE9ntGsPKXkYbtsoVw7iJz9L9VS4R \\
Theory Prop Id: & be594831fd63fc200596d913b2146b4087df4d853a5d72bbbec93372920c5c06 \\
Theory Prop Address: & TMPDzSNyQDmjStN75qX6xofhPvz45wh64pJ
\end{tabular}
\end{center}

\end{theorem}
\section{Basic Results about Fields} % Field2
\begin{theorem}\label{thm:dhfhcgggjgfgmgegpfchfgggmg} ${\unicdcdadad Fs .  {{{\mname{Field}}~{Fs}}\unicdbdjdcd{{{\mname{subfield}}~{Fs}}~{Fs}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0eb1f1396b31417610ee278fb6a8b8d8cdd140a8eedf731088c361bd94a2e7f0 \\
Pure Prop Address: & TMQXDmjHytbWQAqPJjgqXLMDq8SMfVBrMVy \\
Theory Prop Id: & 463bacb9ffd8a7c1e580b20d409cb1f1185318cd2fcd9c728d149096a959c4f5 \\
Theory Prop Address: & TMbHGwwWjrPBorTYyXRmvsBmdT2tyD2ziXc
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dhfhcgggjgfgmgegpfehchbg} ${\unicdcdadad Fs Fs' Fs'' .  {{{{\mname{subfield}}~{Fs}}~{Fs'}}\unicdbdjdcd{{{{\mname{subfield}}~{Fs'}}~{Fs''}}\unicdbdjdcd{{{\mname{subfield}}~{Fs}}~{Fs''}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 66345481ffe8c4fd4fbb8f011c765a0d87adab31bcd77023511f6539b528d18e \\
Pure Prop Address: & TMM11DSqtT24FeA4LM8aLCBtypoFCW7Y25E \\
Theory Prop Id: & 98a2debbf6e60c86f06666f4d0a11ec1170a4b003c3f6f6ac2a0dbc3da02a741 \\
Theory Prop Address: & TMGnVRkmmsKG3BTL5eNCc52GyUUvBzfgjLe
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:gejgfgmgegpffgihehfgogdhjgpgogpfcgjhpfbd}
$\mname{Field\_extension\_by\_1}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 15c0a3060fb3ec8e417c48ab46cf0b959c315076fe1dc011560870c5031255de \\
Pure Object Address: & TMQQtdP8BXq6yrNPjAqW2TErHDrTMXXAnHf \\
Theory Object Id: & 937edba4a112338c9bd442b454c3d9930703191cb45b86271c395bc54d538d82 \\
Theory Object Address: & TMKZ3FEYqeFEFtGCpBAd1kYajCJ4YnCDYCB
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:gejgfgmgegpffgihehfgogdhjgpgogpfcgjhpfbdpfje} ${\unicdcdadad Fs Fs' a .  {{{{\mname{subfield}}~{Fs}}~{Fs'}}\unicdbdjdcd{{{a} \in {{{\mname{Field\_carrier}}~{Fs'}}\unicdcdbdgd{{\mname{Field\_carrier}}~{Fs}}}}\unicdbdjdcd{{({\unicdcdadad Fs'' .  {{{{\mname{subfield}}~{Fs}}~{Fs''}}\unicdbdjdcd{{{a} \in {{\mname{Field\_carrier}}~{Fs''}}}\unicdbdjdcd{{{\mname{subfield}}~{Fs'}}~{Fs''}}}}})}\unicdbdjdcd{{{{\mname{Field\_extension\_by\_1}}~{Fs}}~{Fs'}}~{a}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b32e90df057fb63c1ad17c2a471f552dc5c42a3b49ce631d182cc17768c8ce16 \\
Pure Prop Address: & TMTostbVVVe1Wc1NFks4m8cRXEwnEtFnycJ \\
Theory Prop Id: & d5557b3eb7f49b4ddec41d07f1d23e0b1ce4f8e7657a1c751d122b54af9fa41b \\
Theory Prop Address: & TMPm9E17AXXZrMjJG29R9UHEicjTbN2gajj
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpffgihehfgogdhjgpgogpfcgjhpfbdpffe} ${\unicdcdadad Fs Fs' a .  {{{{{\mname{Field\_extension\_by\_1}}~{Fs}}~{Fs'}}~{a}}\unicdbdjdcd{\unicdcdadad p : {o} .  {{({{{{\mname{subfield}}~{Fs}}~{Fs'}}\unicdbdjdcd{{{a} \in {{{\mname{Field\_carrier}}~{Fs'}}\unicdcdbdgd{{\mname{Field\_carrier}}~{Fs}}}}\unicdbdjdcd{{({\unicdcdadad Fs'' .  {{{{\mname{subfield}}~{Fs}}~{Fs''}}\unicdbdjdcd{{{a} \in {{\mname{Field\_carrier}}~{Fs''}}}\unicdbdjdcd{{{\mname{subfield}}~{Fs'}}~{Fs''}}}}})}\unicdbdjdcd{p}}}})}\unicdbdjdcd{p}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 338a5505ed42a91cb5fa5ec6ab0cf4e76ba17cac12e25143d21eb1cd650c46da \\
Pure Prop Address: & TMNZzAKhVJ6yFrUHhoMKiupzbWxqEfPoy4J \\
Theory Prop Id: & beafbae6117b463b1efc7ff06cf528539b2a460a7d5e21e7589a7e1d18fa1642 \\
Theory Prop Address: & TMFdxk4XGCyjeLqB2oApjE5fghNi2pqqZLN
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:chbgegjgdgbgmgpfggjgfgmgegpffgihehfgogdhjgpgog}
$\mname{radical\_field\_extension}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 4b1aa61ecf07fd27a8a97a4f5ac5a6df80f2d3ad5f55fc4cc58e6d3e76548591 \\
Pure Object Address: & TMchEBbJiTrZFrworejH2faUQ47yR2qjVUh \\
Theory Object Id: & 816f6d770c8c6df637703bbfd5f2ee005e7474a4930bf0953ebe06dca050d7cf \\
Theory Object Address: & TMZ6XfW5b4iotXcF9javzfEe6WjNPU9qL1w
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:chbgegjgdgbgmgpfggjgfgmgegpffgihehfgogdhjgpgogpfje} ${\unicdcdadad Fs Fs' .  {\unicdcdadad r \in {\mname{omega}} .  {\unicdcdadad Fseq .  {{{{Fseq}~{0}}={Fs}}\unicdbdjdcd{{{{Fseq}~{r}}={Fs'}}\unicdbdjdcd{{({\unicdcdadad i \in {{\mname{ordsucc}}~{r}} .  {{\mname{Field}}~{({{Fseq}~{i}})}}})}\unicdbdjdcd{{({\unicdcdadad i \in {r} .  {\unicdcdaddd a \in {{\mname{Field\_carrier}}~{({{Fseq}~{({{\mname{ordsucc}}~{i}})}})}} .  {\unicdcdaddd n \in {\mname{omega}} .  {{{{{{\mname{CRing\_with\_id\_omega\_exp}}~{({{Fseq}~{({{\mname{ordsucc}}~{i}})}})}}~{a}}~{n}} \in {{\mname{Field\_carrier}}~{({{Fseq}~{i}})}}}\unicdcdcdhd{{{{\mname{Field\_extension\_by\_1}}~{({{Fseq}~{i}})}}~{({{Fseq}~{({{\mname{ordsucc}}~{i}})}})}}~{a}}}}}})}\unicdbdjdcd{{{\mname{radical\_field\_extension}}~{Fs}}~{Fs'}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4e422a257d6bf13415f526581580edf290299362d88de0af188ed0d16b294fc0 \\
Pure Prop Address: & TMaTmGPiv6voz3uCpKzxGcrY1beeHKnr1k9 \\
Theory Prop Id: & 6bd73bdf40cf6c2ecf949365a2d93d0d579cef5aa7319b45b404b1739d97e812 \\
Theory Prop Address: & TMb2ezs3LpjpMQYPEQvK9PUQE6aN6HjXb27
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:chbgegjgdgbgmgpfggjgfgmgegpffgihehfgogdhjgpgogpffe} ${\unicdcdadad Fs Fs' .  {{{{\mname{radical\_field\_extension}}~{Fs}}~{Fs'}}\unicdbdjdcd{\unicdcdadad p : {o} .  {{({{{\mname{Field}}~{Fs}}\unicdbdjdcd{{{\mname{Field}}~{Fs'}}\unicdbdjdcd{{{{\mname{subfield}}~{Fs}}~{Fs'}}\unicdbdjdcd{\unicdcdadad r \in {\mname{omega}} .  {\unicdcdadad Fseq .  {{{{Fseq}~{0}}={Fs}}\unicdbdjdcd{{{{Fseq}~{r}}={Fs'}}\unicdbdjdcd{{({\unicdcdadad i \in {{\mname{ordsucc}}~{r}} .  {{\mname{Field}}~{({{Fseq}~{i}})}}})}\unicdbdjdcd{{({\unicdcdadad i \in {{\mname{ordsucc}}~{r}} .  {\unicdcdadad j \in {{\mname{ordsucc}}~{i}} .  {{{\mname{subfield}}~{({{Fseq}~{j}})}}~{({{Fseq}~{i}})}}}})}\unicdbdjdcd{{({\unicdcdadad i \in {r} .  {\unicdcdaddd a \in {{\mname{Field\_carrier}}~{({{Fseq}~{({{\mname{ordsucc}}~{i}})}})}} .  {\unicdcdaddd n \in {\mname{omega}} .  {{{{{{\mname{CRing\_with\_id\_omega\_exp}}~{({{Fseq}~{({{\mname{ordsucc}}~{i}})}})}}~{a}}~{n}} \in {{\mname{Field\_carrier}}~{({{Fseq}~{i}})}}}\unicdcdcdhd{{{{\mname{Field\_extension\_by\_1}}~{({{Fseq}~{i}})}}~{({{Fseq}~{({{\mname{ordsucc}}~{i}})}})}}~{a}}}}}})}\unicdbdjdcd{p}}}}}}}}}}})}\unicdbdjdcd{p}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 04aa436465678920b287c7c3b096ec8a8ad9f9429cfbf92c410bebfde430692d \\
Pure Prop Address: & TMKr8e5rQhQ1BMfoiUXe73gTjPvh5qaip7V \\
Theory Prop Id: & 89a63147cae765b2eabc9cc755f1a4a6c0b4b6c6791569bb6a8e0ed9bd00f0fd \\
Theory Prop Address: & TMYAut45JZbtAUu8e69Mdhf8jq8dSnpBN3M
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:gejgfgmgegpfbgfhehpgngpgchahigjgdhngpfggjgihjgoghg}
$\mname{Field\_automorphism\_fixing}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 55cacef892af061835859ed177e5442518c93eb7ee28697cde3deaec5eafbf01 \\
Pure Object Address: & TMN78iPppPwcxR2NUi3dP5EVHayaxwFwfWr \\
Theory Object Id: & 8e98c0485c8e7d57eb3687ec81bbf72649aea6f54b04d8a845c0664d3392f858 \\
Theory Object Address: & TMFfKJ2CTJMaiuRS28eKxgU3frsxPZBoTum
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:gejgfgmgegpfbgfhehpgngpgchahigjgdhngpfggjgihjgoghgpfje} ${\unicdcdadad K F f .  {{{{\mname{subfield}}~{F}}~{K}}\unicdbdjdcd{{{{{\mname{Field\_Hom}}~{K}}~{K}}~{f}}\unicdbdjdcd{{({\unicdcdadad y \in {{K}~{0}} .  {\unicdcdaddd x \in {{K}~{0}} .  {{{f}~{x}}={y}}}})}\unicdbdjdcd{{({\unicdcdadad x \in {{F}~{0}} .  {{{f}~{x}}={x}}})}\unicdbdjdcd{{{{\mname{Field\_automorphism\_fixing}}~{K}}~{F}}~{f}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8f616dfe39b72caefcdc6aabcb73389242f81b1a7364f5444e6672294fc7a13d \\
Pure Prop Address: & TMSoh1Y12vBR6CW3KxCXhcWQZd5A1FZq1cU \\
Theory Prop Id: & b928875c73ac27a404acf23ab1966ddfcc532a64ee21fb30dd9d57314756729b \\
Theory Prop Address: & TMaXJQsntpr39fhBWDxXZwk8s6e8PSpYjTR
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfbgfhehpgngpgchahigjgdhngpfggjgihjgoghgpffe} ${\unicdcdadad K F f .  {{{{{\mname{Field\_automorphism\_fixing}}~{K}}~{F}}~{f}}\unicdbdjdcd{\unicdcdadad p : {o} .  {{({{{{\mname{subfield}}~{F}}~{K}}\unicdbdjdcd{{{{{\mname{Field\_Hom}}~{K}}~{K}}~{f}}\unicdbdjdcd{{({\unicdcdadad y \in {{K}~{0}} .  {\unicdcdaddd x \in {{K}~{0}} .  {{{f}~{x}}={y}}}})}\unicdbdjdcd{{({\unicdcdadad x \in {{F}~{0}} .  {{{f}~{x}}={x}}})}\unicdbdjdcd{p}}}}})}\unicdbdjdcd{p}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & abbbec85a4745b7e0f7fca7af4f6c54dc3a65291a67132d9d9848d4338a72eef \\
Pure Prop Address: & TMa3L2FNtNGpWEaV5Ctdc4CtUWWGvbY4cRP \\
Theory Prop Id: & b2509c4f43b6dbea462f25fd32e67cd06f5e46262cb519d918cbb958ec386a98 \\
Theory Prop Address: & TMHuLZV7jdk3tK6t9sNMSxXdPPK7H6k2VGW
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:mgbgngpfdgpgngah}
We define $\mname{lam\_comp}$ to be ${\uniddcgcg A f g .  {\uniddcgcg x \in {A} .  {{f}~{({{g}~{x}})}}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 29d9e2fc6403a0149dee771fde6a2efc8a94f848a3566f3ccd60af2065396289 \\
Pure Object Address: & TMZBHh5NXVkgufPoqMzvVCpRFLW2WdfYiJJ \\
Theory Object Id: & f47cda05aa5549792c42c687ced0171e637154b32dbda20a3dd2065d950abd6f \\
Theory Object Address: & TMT1tRAwqVEGpkkvkUdLo93JTWkuSxofJxU
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:mgbgngpfjgeg}
We define $\mname{lam\_id}$ to be ${\uniddcgcg A .  {\uniddcgcg x \in {A} .  {x}}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 6271864c471837aeded4c4e7dc37b9735f9fc4828a34ac9c7979945da815a3c7 \\
Pure Object Address: & TMTjnAw5cKWKUVsHNJJeNN6CgmY8LpuZiYg \\
Theory Object Id: & 86ccd74f57ceb4f87e01c0731683396877d457448dc5c342c35066e0a38f076b \\
Theory Object Address: & TMPRHK8Wyojj7r7mPHtDjeU6KLQUQfd4mis
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:mgbgngpfdgpgngahpffgihahpfjeog} ${\unicdcdadad A B C .  {\unicdcdadad f \in {{B}^{{A}}} .  {\unicdcdadad g \in {{C}^{{B}}} .  {{{{{\mname{lam\_comp}}~{A}}~{g}}~{f}} \in {{C}^{{A}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a368c0a62f8223dcdf075df5f370b455c9b5fc97a3edf8807b478842be43c4f7 \\
Pure Prop Address: & TMGg18zcz7ghZbezgKuURXy33FhGmmAWbXm \\
Theory Prop Id: & 4fede2b31459edc9b94436567d1a7a2010f2eee7b82f8cd7fbbdb2b6ad196ec4 \\
Theory Prop Address: & TMHzPAuFt6vTdQEr4t62NpVuDaya4x1nqZK
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:mgbgngpfjgegpffgihahpfjeog} ${\unicdcdadad A .  {{{\mname{lam\_id}}~{A}} \in {{A}^{{A}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a328f177c58333c407842c44b36358151a17648de6780a0fe94204d0656910eb \\
Pure Prop Address: & TMG2mqqHqLB3YWR1XE3KpoehYhtcgwLGMsh \\
Theory Prop Id: & 025740d37f99a1c2a8b9a6afd977237c7629216ef0f1579ec6fa5bc5a0b22968 \\
Theory Prop Address: & TMdqvc3zfrpqPDraF5Ttxg4ZWaLTYaoRK8c
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:mgbgngpfdgpgngahpfbgdhdhpgdg} ${\unicdcdadad A B .  {\unicdcdadad f \in {{B}^{{A}}} .  {\unicdcdadad g h .  {{{{{\mname{lam\_comp}}~{A}}~{h}}~{({{{{\mname{lam\_comp}}~{A}}~{g}}~{f}})}}={{{{\mname{lam\_comp}}~{A}}~{({{{{\mname{lam\_comp}}~{B}}~{h}}~{g}})}}~{f}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 10d3c2043b57f47398d529842b2b4ef41092863b2ed292e467d739a5a5d48d05 \\
Pure Prop Address: & TMGNEh1ULegqm5w1qTFWfgYNKdQ2N5PWfL3 \\
Theory Prop Id: & 51ef710d91519b6ae4f1e6c1240232977314be4a5e218f254330dc6c7b0e7fb2 \\
Theory Prop Address: & TMX7HYhhWwwEmvKudmWCRyNh3vcLzY4xMPJ
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:mgbgngpfdgpgngahpfjgegpfme} ${\unicdcdadad A B .  {\unicdcdadad f \in {{B}^{{A}}} .  {{{{{\mname{lam\_comp}}~{A}}~{({{\mname{lam\_id}}~{B}})}}~{f}}={f}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e63b276d423c5ffa382e3d24fff1281fc5d23cdc2de80558f7664c37ab8eed29 \\
Pure Prop Address: & TMbj9gKjk5JQsbDmoPhorvNQU4Jq7DGrLwD \\
Theory Prop Id: & 64750339f13b14b1eca32c23b90fa53b58a24aa24d334fb3e2b45602882f363c \\
Theory Prop Address: & TMNXXqZFWBCWcQvn8czxiCArUPkXVyGAsqm
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:mgbgngpfdgpgngahpfjgegpfcf} ${\unicdcdadad A B .  {\unicdcdadad f \in {{B}^{{A}}} .  {{{{{\mname{lam\_comp}}~{A}}~{f}}~{({{\mname{lam\_id}}~{A}})}}={f}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0acec29b4958df486c134fef66fff2628d976311a127b9e66e47d31dce87a2b5 \\
Pure Prop Address: & TMMEAAXiHtjyoC9UixZUX89czksUW4L2AbP \\
Theory Prop Id: & b8b0cd7ab3f2745fc54a89466dffe557184df20469638425a99e0d6af17cc7cf \\
Theory Prop Address: & TMPrbzDNKGk5rH6cAEX3uuwsRXfYLypKbkq
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfiepgngpfjgeg} ${\unicdcdadad F .  {{{\mname{Field}}~{F}}\unicdbdjdcd{{{{\mname{Field\_Hom}}~{F}}~{F}}~{({{\mname{lam\_id}}~{({{F}~{0}})}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e76108b7394a2d0ef4a23eeff5c2eff0a59bfd099b41a3efcf63c829da51cd0e \\
Pure Prop Address: & TMMTreDckMCE8QUxnfjGRBucakRyKZDd5Uw \\
Theory Prop Id: & 0a051badc75ad444016ac67529bbfa1ebe66ca5459cd8875e236240cb319fd29 \\
Theory Prop Address: & TMbgZLG5jAx7kLyryCTxrpfmKu9WndjBQKz
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:gejgfgmgegpfiepgngpfdgpgngah} ${\unicdcdadad F F' F'' g h .  {{{{{\mname{Field\_Hom}}~{F}}~{F'}}~{g}}\unicdbdjdcd{{{{{\mname{Field\_Hom}}~{F'}}~{F''}}~{h}}\unicdbdjdcd{{{{\mname{Field\_Hom}}~{F}}~{F''}}~{({{{{\mname{lam\_comp}}~{({{F}~{0}})}}~{h}}~{g}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f96e7b8972ab6ddc476b85f43c26f21233bb2d05a4284718f987e06e5bb0a539 \\
Pure Prop Address: & TMXHqDN9vGwVX2JmvbvZuV4Jx7aQ6ptioS9 \\
Theory Prop Id: & c7176150678884e662532193f41ddefed41f8c69c784867e0e5e7599cfccc3d7 \\
Theory Prop Address: & TMFHd96nKERMA8xrf6a4PPnaFSZAyhMgQkd
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:hebgmgpgjgdhpfhechpgfhah}
We define $\mname{Galois\_Group}$ to be ${\uniddcgcg K F .  {{{\mname{pack\_b}}~{\{f \in {{{K}~{0}}^{{{K}~{0}}}}|{{{{\mname{Field\_automorphism\_fixing}}~{K}}~{F}}~{f}}\}}}~{({{\mname{lam\_comp}}~{({{K}~{0}})}})}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 831192b152172f585e3b6d9b53142cba7a2d8becdffe4e6337c037c027e01e21 \\
Pure Object Address: & TMYqxuc9rAFqZk2CRVHyc2y7pfNsCZU6equ \\
Theory Object Id: & ca458a9929d10327f6d82d25599b1037bc98c2bdf117e527489c6a4d6ffdd167 \\
Theory Object Address: & TMTJqgfvRfobXKQitP5Ljdprk53Cpq27TKH
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:hebgmgpgjgdhpfhechpgfhahpfad} ${\unicdcdadad K F .  {{{{{\mname{Galois\_Group}}~{K}}~{F}}~{0}}={\{f \in {{{K}~{0}}^{{{K}~{0}}}}|{{{{\mname{Field\_automorphism\_fixing}}~{K}}~{F}}~{f}}\}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c937d2405bc02024b3013de5808dbe9e3504c142d376d7ff1ca27d63e12e562e \\
Pure Prop Address: & TMP5RNZvDusyH2t1cf286riba2LdRzc1YJv \\
Theory Prop Id: & efd193beaee2e86f35612249b45870a142e7e8c50719336225df8ef19e54b2d9 \\
Theory Prop Address: & TMHr9KDkArCoQ1vA2dUxzDwknQj6pDMv7LB
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:hebgmgpgjgdhpfhechpgfhahpfhechpgfhah} ${\unicdcdadad F K .  {{{{\mname{subfield}}~{F}}~{K}}\unicdbdjdcd{{\mname{Group}}~{({{{\mname{Galois\_Group}}~{K}}~{F}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 23e81a79edfd40eff87623569e69d5d6bd17fea035e30db29d3fa252dc9292df \\
Pure Prop Address: & TMF8s32NGdaXaUxYsMdcKNoMmb1qtqso9ph \\
Theory Prop Id: & ed4e90cd2b4fa72539381db20b559cb765274456c2523b29855fe21eefb0bf54 \\
Theory Prop Address: & TMZrV2L74MSsae3E5TMtqrcs8St33ZF5Hbo
\end{tabular}
\end{center}

\end{theorem}
\section{explicit\_Reals\_transfer}\label{fgihahmgjgdgjgehpfcffgbgmgdhpfehchbgogdhggfgch}Let $ R : {\iota}$ be given.
Let $ zero one : {\iota}$ be given.
Let $ plus mult : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${plus}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${mult}$.
Let $ leq : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ be given.
{\bf{Notation.}} We use $\infmdnd$ as an infix operator  corresponding to applying term ${leq}$.
Let $ R' : {\iota}$ be given.
Let $ zero' one' : {\iota}$ be given.
Let $ plus' mult' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\infkdlckd$ as a right associative infix operator  corresponding to applying term ${plus'}$.
{\bf{Notation.}} We use $\infkdkckd$ as a right associative infix operator  corresponding to applying term ${mult'}$.
Let $ leq' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ be given.
Let $ f : {{\iota}\unicdbdjdcd{\iota}}$ be given.
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcffgbgmgdhpfehchbgogdhggfgch} ${{{{{{{{\mname{explicit\_Reals}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}~{leq}}\unicdbdjdcd{{{{{\mname{bij}}~{R}}~{R'}}~{f}}\unicdbdjdcd{{{{f}~{zero}}={zero'}}\unicdbdjdcd{{{{f}~{one}}={one'}}\unicdbdjdcd{{({\unicdcdadad x y \in {R} .  {{{f}~{({{x}+{y}})}}={{{f}~{x}}\uniadadcdcg{{f}~{y}}}}})}\unicdbdjdcd{{({\unicdcdadad x y \in {R} .  {{{f}~{({{x}*{y}})}}={{{f}~{x}}\unicdbgcdgg{{f}~{y}}}}})}\unicdbdjdcd{{({\unicdcdadad x y \in {R} .  {{{x}\unicdcdgded{y}}\unicdbdjded{{{leq'}~{({{f}~{x}})}}~{({{f}~{y}})}}}})}\unicdbdjdcd{{{{{{{\mname{explicit\_Reals}}~{R'}}~{zero'}}~{one'}}~{plus'}}~{mult'}}~{leq'}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & eab1221701cf6d740b9b72782e98f152a3f7f2cdf16638d049fc649d996fc29c \\
Pure Prop Address: & TMYhyMVVJTvxXty5NxJVswTmqpdUcPwJ3PN \\
Theory Prop Id: & 76534117383e5ea208dccdd5106698afc06e708ae05d009cb0e347dfd0cf2ae2 \\
Theory Prop Address: & TMY35GcU6u4DUqWLoorNqpUAYwMdFLABjvj
\end{tabular}
\end{center}

\end{theorem}
