\documentclass{article}
\newtheorem{axiom}{Axiom}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{proposition}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{example}{Example}
\newtheorem{conjecture}{Conjecture}
\newcommand\unicdcdgdad{\not=}
\newcommand\unicdcdcdbg{\cup}
\newcommand\unicdcdbdgd{\setminus}
\newcommand\unicdcdcdjd{\cap}
\newcommand\unicdcdadad{\forall}
\newcommand\unicdbdjdcd{\Rightarrow}
\newcommand\unicdcdadjd{\notin}
\newcommand\unicdbdjded{\Leftrightarrow}
\newcommand\unicdcdcdid{\lor}
\newcommand\unicdcdcdhd{\land}
\newcommand\uniddcgcg{\lambda}
\newcommand\unicdcdaddd{\exists}
\newcommand\unicdcdidid{\not\subseteq}
\newcommand\preoh[1]{\lnot #1}
\newcommand\mname[1]{{\mathsf{#1}}}
\begin{document}
\title{t13\_gr\_cy\_1 (TMMAd9eGJG5svngHA8oT5kcTtpQmabN4XEn)}
\maketitle
Let $ k1\_group\_1 : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Let $ k2\_gr\_cy\_1 : {\iota}$ be given.
Let $ k6\_numbers : {\iota}$ be given.
Let $ v2\_struct\_0 : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ v2\_group\_1 : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ l3\_algstr\_0 : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ m1\_subset\_1 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{o}}}$ be given.
Let $ u1\_struct\_0 : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Let $ k6\_algstr\_0 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}}$ be given.
Let $ k1\_xboole\_0 : {\iota}$ be given.
Let $ k4\_ordinal1 : {\iota}$ be given.
Let $ v1\_xcmplx\_0 : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ k2\_xcmplx\_0 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}$ be given.
Let $ v1\_int\_1 : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ k20\_binop\_2 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}$ be given.
Let $ v1\_funct\_1 : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ v1\_funct\_2 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{o}}}}$ be given.
Let $ k2\_zfmisc\_1 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}$ be given.
Let $ k1\_zfmisc\_1 : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Let $ g3\_algstr\_0 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}$ be given.
Let $ v6\_membered : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ v5\_membered : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ k4\_numbers : {\iota}$ be given.
Let $ v15\_algstr\_0 : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ v3\_group\_1 : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ k44\_binop\_2 : {\iota}$ be given.
Let $ v3\_membered : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ v1\_membered : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ v4\_membered : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ v7\_ordinal1 : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ u2\_algstr\_0 : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  ((\preoh v2\_struct\_0~X0){\unicdcdcdhd}((v2\_group\_1~X0){\unicdcdcdhd}(l3\_algstr\_0~\\
X0))){\unicdbdjdcd}({\unicdcdadad} X1 .  (m1\_subset\_1~X1~(u1\_struct\_0~X0)){\unicdbdjdcd}(({\unicdcdadad} X2 .  \\
(m1\_subset\_1~X2~(u1\_struct\_0~X0)){\unicdbdjdcd}((k6\_algstr\_0~X0~X2~X1=X2){\unicdcdcdhd}\\
(k6\_algstr\_0~X0~X1~X2=X2))){\unicdbdjdcd}(X1=k1\_group\_1~X0)))\end{array}
\label{hyp:ehedpfhgchpgfhahpfbd}
\end{equation}
Assume the following.
\begin{equation}
{{\unicdcdadad} X0 .  {{\unicdcdadad} X1 .  {{({{X0} \in {X1}})}{\unicdbdjdcd}{({{{m1\_subset\_1}~{X0}}~{X1}})}}}}\label{hyp:ehbdpfdhfhcgdhfgeh}
\end{equation}
Assume the following.
\begin{equation}
{{{m1\_subset\_1}~{k1\_xboole\_0}}~{k4\_ordinal1}}\label{hyp:ehbdpfogfhngfgchbgmgdh}
\end{equation}
Assume the following.
\begin{equation}
{{\unicdcdadad} X0 .  {{({{v1\_xcmplx\_0}~{X0}})}{\unicdbdjdcd}{({{{{k2\_xcmplx\_0}~{X0}}~{k6\_numbers}}={X0}})}}}\label{hyp:ehbdpfbgchjgehigng}
\end{equation}
Assume the following.
\begin{equation}
{{k6\_numbers}={k1\_xboole\_0}}\label{hyp:chfgegfgggjgogjgehjgpgogpflggdpfogfhngcgfgchdh}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  {\unicdcdadad} X1 .  ((v1\_int\_1~X0){\unicdcdcdhd}(v1\_int\_1~X1)){\unicdbdjdcd}(k20\_binop\_2~\\
X0~X1=k2\_xcmplx\_0~X0~X1)\end{array}
\label{hyp:chfgegfgggjgogjgehjgpgogpflgcdadpfcgjgogpgahpfcd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  {\unicdcdadad} X1 .  ((m1\_subset\_1~X0~(u1\_struct\_0~k2\_gr\_cy\_1)){\unicdcdcdhd}\\
(m1\_subset\_1~X1~(u1\_struct\_0~k2\_gr\_cy\_1))){\unicdbdjdcd}(k6\_algstr\_0~k2\_gr\_cy\_1~\\
X0~X1=k20\_binop\_2~X0~X1)\end{array}
\label{hyp:jgfgbdpfhgchpfdgjhpfbd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  {\unicdcdadad} X1 .  ((v1\_funct\_1~X1){\unicdcdcdhd}((v1\_funct\_2~X1~(k2\_zfmisc\_1~\\
X0~X0)~X0){\unicdcdcdhd}(m1\_subset\_1~X1~(k1\_zfmisc\_1~(k2\_zfmisc\_1~(k2\_zfmisc\_1~\\
X0~X0)~X0))))){\unicdbdjdcd}({\unicdcdadad} X2 .  {\unicdcdadad} X3 .  (g3\_algstr\_0~X0~X1=g3\_algstr\_0~\\
X2~X3){\unicdbdjdcd}((X0=X2){\unicdcdcdhd}(X1=X3)))\end{array}
\label{hyp:ggchfgfgpfhgddpfbgmghgdhehchpfad}
\end{equation}
Assume the following.
\begin{equation}
{{v6\_membered}~{k4\_ordinal1}}\label{hyp:ggdggdpfngfgngcgfgchfgeg}
\end{equation}
Assume the following.
\begin{equation}
{{v5\_membered}~{k4\_numbers}}\label{hyp:ggdgfdpfngfgngcgfgchfgeg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}(\preoh v2\_struct\_0~k2\_gr\_cy\_1){\unicdcdcdhd}((v15\_algstr\_0~k2\_gr\_cy\_1){\unicdcdcdhd}((v2\_group\_1~\\
k2\_gr\_cy\_1){\unicdcdcdhd}(v3\_group\_1~k2\_gr\_cy\_1)))\end{array}
\label{hyp:ggdgedpfhgchpfdgjhpfbd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}(v1\_funct\_1~k44\_binop\_2){\unicdcdcdhd}((v1\_funct\_2~k44\_binop\_2~(k2\_zfmisc\_1~\\
k4\_numbers~k4\_numbers)~k4\_numbers){\unicdcdcdhd}(m1\_subset\_1~k44\_binop\_2~\\
(k1\_zfmisc\_1~(k2\_zfmisc\_1~(k2\_zfmisc\_1~k4\_numbers~k4\_numbers)~\\
k4\_numbers))))\end{array}
\label{hyp:egehpflgededpfcgjgogpgahpfcd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}(\preoh v2\_struct\_0~k2\_gr\_cy\_1){\unicdcdcdhd}((v15\_algstr\_0~k2\_gr\_cy\_1){\unicdcdcdhd}(l3\_algstr\_0~\\
k2\_gr\_cy\_1))\end{array}
\label{hyp:egehpflgcdpfhgchpfdgjhpfbd}
\end{equation}
Assume the following.
\begin{equation}
{{k2\_gr\_cy\_1}={{{g3\_algstr\_0}~{k4\_numbers}}~{k44\_binop\_2}}}\label{hyp:egddpfhgchpfdgjhpfbd}
\end{equation}
Assume the following.
\begin{equation}
{{\unicdcdadad} X0 .  {{({{v1\_int\_1}~{X0}})}{\unicdbdjded}{({{X0} \in {k4\_numbers}})}}}\label{hyp:egcdpfjgogehpfbd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  {\unicdcdadad} X1 .  ((v1\_int\_1~X0){\unicdcdcdhd}(v1\_int\_1~X1)){\unicdbdjdcd}(k20\_binop\_2~\\
X0~X1=k20\_binop\_2~X1~X0)\end{array}
\label{hyp:dgpgngngfhehbgehjgghjgehjhpflgcdadpfcgjgogpgahpfcd}
\end{equation}
Assume the following.
\begin{equation}
{{\unicdcdadad} X0 .  {{({{v3\_membered}~{X0}})}{\unicdbdjdcd}{({{v1\_membered}~{X0}})}}}\label{hyp:dgdgfdpfngfgngcgfgchfgeg}
\end{equation}
Assume the following.
\begin{equation}
{{\unicdcdadad} X0 .  {{({{v4\_membered}~{X0}})}{\unicdbdjdcd}{({{v3\_membered}~{X0}})}}}\label{hyp:dgdgddpfngfgngcgfgchfgeg}
\end{equation}
Assume the following.
\begin{equation}
{{\unicdcdadad} X0 .  {{({{v5\_membered}~{X0}})}{\unicdbdjdcd}{({{v4\_membered}~{X0}})}}}\label{hyp:dgdgcdpfngfgngcgfgchfgeg}
\end{equation}
Assume the following.
\begin{equation}
{{\unicdcdadad} X0 .  {{({{v7\_ordinal1}~{X0}})}{\unicdbdjdcd}{({{v1\_int\_1}~{X0}})}}}\label{hyp:dgdgcdpfjgogehpfbd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  (v6\_membered~X0){\unicdbdjdcd}({\unicdcdadad} X1 .  (m1\_subset\_1~X1~X0){\unicdbdjdcd}\\
(v7\_ordinal1~X1))\end{array}
\label{hyp:dgdgbdhdpfngfgngcgfgchfgeg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  (v5\_membered~X0){\unicdbdjdcd}({\unicdcdadad} X1 .  (m1\_subset\_1~X1~X0){\unicdbdjdcd}\\
(v1\_int\_1~X1))\end{array}
\label{hyp:dgdgbdgdpfngfgngcgfgchfgeg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  (v1\_membered~X0){\unicdbdjdcd}({\unicdcdadad} X1 .  (m1\_subset\_1~X1~X0){\unicdbdjdcd}\\
(v1\_xcmplx\_0~X1))\end{array}
\label{hyp:dgdgbdcdpfngfgngcgfgchfgeg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  (l3\_algstr\_0~X0){\unicdbdjdcd}((v15\_algstr\_0~X0){\unicdbdjdcd}(X0=g3\_algstr\_0~\\
(u1\_struct\_0~X0)~(u2\_algstr\_0~X0)))\end{array}
\label{hyp:bgcgdhehchbgdgehogfgdhdhpfghbdfdpfbgmghgdhehchpfad}
\end{equation}
\begin{theorem}\label{thm:ehbdddpfhgchpfdgjhpfbd}
${{{k1\_group\_1}~{k2\_gr\_cy\_1}}={k6\_numbers}}$.
\end{theorem}
\end{document}
