:: MOD_2 semantic presentation begin definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); func :::"TrivialLMod"::: "R" -> ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"LeftMod":::) "of" "R" equals :: MOD_2:def 1 (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "," (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") "," (Num 1) ")" ")" ) "#)" ); end; :: deftheorem defines :::"TrivialLMod"::: MOD_2:def 1 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k1_mod_2 :::"TrivialLMod"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "," (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Num 1) ")" ")" ) "#)" ))); theorem :: MOD_2:1 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k1_mod_2 :::"TrivialLMod"::: ) (Set (Var "R")) ")" ) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k1_mod_2 :::"TrivialLMod"::: ) (Set (Var "R")) ")" ))))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "G", "H" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "R")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "G")) "," (Set (Const "H")); attr "f" is :::"homogeneous"::: means :: MOD_2:def 2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Scalar":::) "of" "R" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vector":::) "of" "G" "holds" (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))); end; :: deftheorem defines :::"homogeneous"::: MOD_2:def 2 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "R")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_mod_2 :::"homogeneous"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ")" )))); theorem :: MOD_2:2 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "R")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "H")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_mod_2 :::"homogeneous"::: ) ) & (Bool (Set (Var "g")) "is" ($#v1_mod_2 :::"homogeneous"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#v1_mod_2 :::"homogeneous"::: ) ))))) ; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); let "G", "H" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); cluster (Set ($#k6_grcat_1 :::"ZeroMap"::: ) "(" "G" "," "H" ")" ) -> ($#v1_mod_2 :::"homogeneous"::: ) ; end; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); attr "c2" is :::"strict"::: ; struct :::"LModMorphismStr"::: "over" "R" -> ; aggr :::"LModMorphismStr":::(# :::"Dom":::, :::"Cod":::, :::"Fun"::: #) -> ($#l1_mod_2 :::"LModMorphismStr"::: ) "over" "R"; sel :::"Dom"::: "c2" -> ($#l1_vectsp_1 :::"LeftMod":::) "of" "R"; sel :::"Cod"::: "c2" -> ($#l1_vectsp_1 :::"LeftMod":::) "of" "R"; sel :::"Fun"::: "c2" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_mod_2 :::"Dom"::: ) "of" "c2") "," (Set "the" ($#u2_mod_2 :::"Cod"::: ) "of" "c2"); end; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "f" be ($#l1_mod_2 :::"LModMorphismStr"::: ) "over" (Set (Const "R")); func :::"dom"::: "f" -> ($#l1_vectsp_1 :::"LeftMod":::) "of" "R" equals :: MOD_2:def 3 (Set "the" ($#u1_mod_2 :::"Dom"::: ) "of" "f"); func :::"cod"::: "f" -> ($#l1_vectsp_1 :::"LeftMod":::) "of" "R" equals :: MOD_2:def 4 (Set "the" ($#u2_mod_2 :::"Cod"::: ) "of" "f"); end; :: deftheorem defines :::"dom"::: MOD_2:def 3 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "f")) "being" ($#l1_mod_2 :::"LModMorphismStr"::: ) "over" (Set (Var "R")) "holds" (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_mod_2 :::"Dom"::: ) "of" (Set (Var "f")))))); :: deftheorem defines :::"cod"::: MOD_2:def 4 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "f")) "being" ($#l1_mod_2 :::"LModMorphismStr"::: ) "over" (Set (Var "R")) "holds" (Bool (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_mod_2 :::"Cod"::: ) "of" (Set (Var "f")))))); definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "f" be ($#l1_mod_2 :::"LModMorphismStr"::: ) "over" (Set (Const "R")); func :::"fun"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_mod_2 :::"dom"::: ) "f" ")" ) "," (Set "(" ($#k3_mod_2 :::"cod"::: ) "f" ")" ) equals :: MOD_2:def 5 (Set "the" ($#u3_mod_2 :::"Fun"::: ) "of" "f"); end; :: deftheorem defines :::"fun"::: MOD_2:def 5 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "f")) "being" ($#l1_mod_2 :::"LModMorphismStr"::: ) "over" (Set (Var "R")) "holds" (Bool (Set ($#k4_mod_2 :::"fun"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_mod_2 :::"Fun"::: ) "of" (Set (Var "f")))))); theorem :: MOD_2:3 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "f")) "being" ($#l1_mod_2 :::"LModMorphismStr"::: ) "over" (Set (Var "R")) (Bool "for" (Set (Var "f0")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "f0")) "#)" ))) "holds" (Bool "(" (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "G1"))) & (Bool (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "G2"))) & (Bool (Set ($#k4_mod_2 :::"fun"::: ) (Set (Var "f"))) ($#r1_funct_2 :::"="::: ) (Set (Var "f0"))) ")" ))))) ; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "G", "H" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); func :::"ZERO"::: "(" "G" "," "H" ")" -> ($#v2_mod_2 :::"strict"::: ) ($#l1_mod_2 :::"LModMorphismStr"::: ) "over" "R" equals :: MOD_2:def 6 (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" "G" "," "H" "," (Set "(" ($#k6_grcat_1 :::"ZeroMap"::: ) "(" "G" "," "H" ")" ")" ) "#)" ); end; :: deftheorem defines :::"ZERO"::: MOD_2:def 6 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_mod_2 :::"ZERO"::: ) "(" (Set (Var "G")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G")) "," (Set (Var "H")) "," (Set "(" ($#k6_grcat_1 :::"ZeroMap"::: ) "(" (Set (Var "G")) "," (Set (Var "H")) ")" ")" ) "#)" )))); definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "IT" be ($#l1_mod_2 :::"LModMorphismStr"::: ) "over" (Set (Const "R")); attr "IT" is :::"LModMorphism-like"::: means :: MOD_2:def 7 (Bool "(" (Bool (Set ($#k4_mod_2 :::"fun"::: ) "IT") "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set ($#k4_mod_2 :::"fun"::: ) "IT") "is" ($#v1_mod_2 :::"homogeneous"::: ) ) ")" ); end; :: deftheorem defines :::"LModMorphism-like"::: MOD_2:def 7 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "IT")) "being" ($#l1_mod_2 :::"LModMorphismStr"::: ) "over" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_mod_2 :::"LModMorphism-like"::: ) ) "iff" (Bool "(" (Bool (Set ($#k4_mod_2 :::"fun"::: ) (Set (Var "IT"))) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set ($#k4_mod_2 :::"fun"::: ) (Set (Var "IT"))) "is" ($#v1_mod_2 :::"homogeneous"::: ) ) ")" ) ")" ))); registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); cluster ($#v2_mod_2 :::"strict"::: ) ($#v3_mod_2 :::"LModMorphism-like"::: ) for ($#l1_mod_2 :::"LModMorphismStr"::: ) "over" "R"; end; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); mode LModMorphism of "R" is ($#v3_mod_2 :::"LModMorphism-like"::: ) ($#l1_mod_2 :::"LModMorphismStr"::: ) "over" "R"; end; theorem :: MOD_2:4 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "F")) "being" ($#l1_mod_2 :::"LModMorphism":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set "the" ($#u3_mod_2 :::"Fun"::: ) "of" (Set (Var "F"))) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set "the" ($#u3_mod_2 :::"Fun"::: ) "of" (Set (Var "F"))) "is" ($#v1_mod_2 :::"homogeneous"::: ) ) ")" ))) ; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); let "G", "H" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); cluster (Set ($#k5_mod_2 :::"ZERO"::: ) "(" "G" "," "H" ")" ) -> ($#v2_mod_2 :::"strict"::: ) ($#v3_mod_2 :::"LModMorphism-like"::: ) ; end; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "G", "H" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); mode :::"Morphism"::: "of" "G" "," "H" -> ($#l1_mod_2 :::"LModMorphism":::) "of" "R" means :: MOD_2:def 8 (Bool "(" (Bool (Set ($#k2_mod_2 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "G") & (Bool (Set ($#k3_mod_2 :::"cod"::: ) it) ($#r1_hidden :::"="::: ) "H") ")" ); end; :: deftheorem defines :::"Morphism"::: MOD_2:def 8 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "b4")) "being" ($#l1_mod_2 :::"LModMorphism":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H"))) "iff" (Bool "(" (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))) ")" ) ")" )))); registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); let "G", "H" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); cluster ($#v2_mod_2 :::"strict"::: ) ($#v3_mod_2 :::"LModMorphism-like"::: ) for ($#m1_mod_2 :::"Morphism"::: ) "of" "G" "," "H"; end; theorem :: MOD_2:5 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "f")) "being" ($#l1_mod_2 :::"LModMorphismStr"::: ) "over" (Set (Var "R")) "st" (Bool (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))) & (Bool (Set ($#k4_mod_2 :::"fun"::: ) (Set (Var "f"))) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set ($#k4_mod_2 :::"fun"::: ) (Set (Var "f"))) "is" ($#v1_mod_2 :::"homogeneous"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")))))) ; theorem :: MOD_2:6 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_mod_2 :::"homogeneous"::: ) )) "holds" (Bool (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "f")) "#)" ) "is" ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")))))) ; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); let "G" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); cluster (Set ($#k3_struct_0 :::"id"::: ) "G") -> ($#v1_mod_2 :::"homogeneous"::: ) ; end; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "G" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); func :::"ID"::: "G" -> ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" "G" "," "G" equals :: MOD_2:def 9 (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" "G" "," "G" "," (Set "(" ($#k3_struct_0 :::"id"::: ) "G" ")" ) "#)" ); end; :: deftheorem defines :::"ID"::: MOD_2:def 9 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k6_mod_2 :::"ID"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G")) "," (Set (Var "G")) "," (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "G")) ")" ) "#)" )))); definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "G", "H" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); :: original: :::"ZERO"::: redefine func :::"ZERO"::: "(" "G" "," "H" ")" -> ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" "G" "," "H"; end; theorem :: MOD_2:7 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "F")) "being" ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool "(" (Bool (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set "the" ($#u1_mod_2 :::"Dom"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u2_mod_2 :::"Cod"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u3_mod_2 :::"Fun"::: ) "of" (Set (Var "F"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "f")) "#)" )) & (Bool (Set (Var "f")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_mod_2 :::"homogeneous"::: ) ) ")" ))))) ; theorem :: MOD_2:8 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "F")) "being" ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "f")) "#)" )))))) ; theorem :: MOD_2:9 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "F")) "being" ($#l1_mod_2 :::"LModMorphism":::) "of" (Set (Var "R")) (Bool "ex" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) "st" (Bool (Set (Var "F")) "is" ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")))))) ; theorem :: MOD_2:10 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "F")) "being" ($#v2_mod_2 :::"strict"::: ) ($#l1_mod_2 :::"LModMorphism":::) "of" (Set (Var "R")) (Bool "ex" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "f")) "#)" )) & (Bool (Set (Var "f")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_mod_2 :::"homogeneous"::: ) ) ")" ))))) ; theorem :: MOD_2:11 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#l1_mod_2 :::"LModMorphism":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "g")) "is" ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G2")) "," (Set (Var "G3"))) & (Bool (Set (Var "f")) "is" ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2"))) ")" )))) ; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "G", "F" be ($#l1_mod_2 :::"LModMorphism":::) "of" (Set (Const "R")); assume (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Const "G"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Const "F")))) ; func "G" :::"*"::: "F" -> ($#v2_mod_2 :::"strict"::: ) ($#l1_mod_2 :::"LModMorphism":::) "of" "R" means :: MOD_2:def 10 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" "R" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G2")) "," (Set (Var "G3")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set "the" ($#u1_mod_2 :::"Dom"::: ) "of" "G") "," (Set "the" ($#u2_mod_2 :::"Cod"::: ) "of" "G") "," (Set "the" ($#u3_mod_2 :::"Fun"::: ) "of" "G") "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "g")) "#)" )) & (Bool (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set "the" ($#u1_mod_2 :::"Dom"::: ) "of" "F") "," (Set "the" ($#u2_mod_2 :::"Cod"::: ) "of" "F") "," (Set "the" ($#u3_mod_2 :::"Fun"::: ) "of" "F") "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "f")) "#)" ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G3")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "#)" ))))); end; :: deftheorem defines :::"*"::: MOD_2:def 10 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#l1_mod_2 :::"LModMorphism":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#v2_mod_2 :::"strict"::: ) ($#l1_mod_2 :::"LModMorphism":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k8_mod_2 :::"*"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G2")) "," (Set (Var "G3")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set "the" ($#u1_mod_2 :::"Dom"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_mod_2 :::"Cod"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u3_mod_2 :::"Fun"::: ) "of" (Set (Var "G"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "g")) "#)" )) & (Bool (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set "the" ($#u1_mod_2 :::"Dom"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u2_mod_2 :::"Cod"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u3_mod_2 :::"Fun"::: ) "of" (Set (Var "F"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "f")) "#)" ))) "holds" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G3")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "#)" ))))) ")" )))); theorem :: MOD_2:12 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "G1")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "G")) "being" ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G2")) "," (Set (Var "G3")) (Bool "for" (Set (Var "F")) "being" ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "holds" (Bool (Set (Set (Var "G")) ($#k8_mod_2 :::"*"::: ) (Set (Var "F"))) "is" ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G1")) "," (Set (Var "G3"))))))) ; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "G1", "G2", "G3" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); let "G" be ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Const "G2")) "," (Set (Const "G3")); let "F" be ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Const "G1")) "," (Set (Const "G2")); func "G" :::"*'"::: "F" -> ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" "G1" "," "G3" equals :: MOD_2:def 11 (Set "G" ($#k8_mod_2 :::"*"::: ) "F"); end; :: deftheorem defines :::"*'"::: MOD_2:def 11 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "G")) "being" ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G2")) "," (Set (Var "G3")) (Bool "for" (Set (Var "F")) "being" ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "holds" (Bool (Set (Set (Var "G")) ($#k9_mod_2 :::"*'"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k8_mod_2 :::"*"::: ) (Set (Var "F")))))))); theorem :: MOD_2:13 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "G1")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "G")) "being" ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G2")) "," (Set (Var "G3")) (Bool "for" (Set (Var "F")) "being" ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G2")) "," (Set (Var "G3")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "g")) "#)" )) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "f")) "#)" ))) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k9_mod_2 :::"*'"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G3")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "#)" )) & (Bool (Set (Set (Var "G")) ($#k8_mod_2 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G3")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "#)" )) ")" ))))))) ; theorem :: MOD_2:14 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v2_mod_2 :::"strict"::: ) ($#l1_mod_2 :::"LModMorphism":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))(Bool "ex" (Set (Var "f0")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G1")) "," (Set (Var "G2"))(Bool "ex" (Set (Var "g0")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G2")) "," (Set (Var "G3")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "f0")) "#)" )) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "g0")) "#)" )) & (Bool (Set (Set (Var "g")) ($#k8_mod_2 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#g1_mod_2 :::"LModMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G3")) "," (Set "(" (Set (Var "g0")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f0")) ")" ) "#)" )) ")" )))))) ; theorem :: MOD_2:15 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v2_mod_2 :::"strict"::: ) ($#l1_mod_2 :::"LModMorphism":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set "(" (Set (Var "g")) ($#k8_mod_2 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_mod_2 :::"cod"::: ) (Set "(" (Set (Var "g")) ($#k8_mod_2 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "g")))) ")" ))) ; theorem :: MOD_2:16 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "G4")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "f")) "being" ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "g")) "being" ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G2")) "," (Set (Var "G3")) (Bool "for" (Set (Var "h")) "being" ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G3")) "," (Set (Var "G4")) "holds" (Bool (Set (Set (Var "h")) ($#k8_mod_2 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k8_mod_2 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k8_mod_2 :::"*"::: ) (Set (Var "g")) ")" ) ($#k8_mod_2 :::"*"::: ) (Set (Var "f"))))))))) ; theorem :: MOD_2:17 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#v2_mod_2 :::"strict"::: ) ($#l1_mod_2 :::"LModMorphism":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "g")))) & (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "h")) ($#k8_mod_2 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k8_mod_2 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k8_mod_2 :::"*"::: ) (Set (Var "g")) ")" ) ($#k8_mod_2 :::"*"::: ) (Set (Var "f")))))) ; theorem :: MOD_2:18 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set "(" ($#k6_mod_2 :::"ID"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set ($#k3_mod_2 :::"cod"::: ) (Set "(" ($#k6_mod_2 :::"ID"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool "(" "for" (Set (Var "f")) "being" ($#v2_mod_2 :::"strict"::: ) ($#l1_mod_2 :::"LModMorphism":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "G")))) "holds" (Bool (Set (Set "(" ($#k6_mod_2 :::"ID"::: ) (Set (Var "G")) ")" ) ($#k8_mod_2 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ) & (Bool "(" "for" (Set (Var "g")) "being" ($#v2_mod_2 :::"strict"::: ) ($#l1_mod_2 :::"LModMorphism":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "g")) ($#k8_mod_2 :::"*"::: ) (Set "(" ($#k6_mod_2 :::"ID"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ) ")" ))) ; theorem :: MOD_2:19 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "UN")) "holds" (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#k1_enumset1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "UN"))))) ; theorem :: MOD_2:20 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "UN")) "holds" (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "u"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "UN"))))) ; theorem :: MOD_2:21 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "UN"))) & (Bool (Num 1) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "UN"))) & (Bool (Num 2) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "UN"))) ")" )) ; definitionlet "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ); func :::"-"::: "a" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) equals :: MOD_2:def 12 (Set ($#k6_numbers :::"0"::: ) ) if (Bool "a" ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) (Num 2) if (Bool "a" ($#r1_hidden :::"="::: ) (Num 1)) (Num 1) if (Bool "a" ($#r1_hidden :::"="::: ) (Num 2)) ; let "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ); func "a" :::"+"::: "b" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) equals :: MOD_2:def 13 "b" if (Bool "a" ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "a" if (Bool "b" ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) (Num 2) if (Bool "(" (Bool "a" ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "b" ($#r1_hidden :::"="::: ) (Num 1)) ")" ) (Set ($#k6_numbers :::"0"::: ) ) if (Bool "(" (Bool "a" ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "b" ($#r1_hidden :::"="::: ) (Num 2)) ")" ) (Set ($#k6_numbers :::"0"::: ) ) if (Bool "(" (Bool "a" ($#r1_hidden :::"="::: ) (Num 2)) & (Bool "b" ($#r1_hidden :::"="::: ) (Num 1)) ")" ) (Num 1) if (Bool "(" (Bool "a" ($#r1_hidden :::"="::: ) (Num 2)) & (Bool "b" ($#r1_hidden :::"="::: ) (Num 2)) ")" ) ; func "a" :::"*"::: "b" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) equals :: MOD_2:def 14 (Set ($#k6_numbers :::"0"::: ) ) if (Bool "b" ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) (Set ($#k6_numbers :::"0"::: ) ) if (Bool "a" ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "a" if (Bool "b" ($#r1_hidden :::"="::: ) (Num 1)) "b" if (Bool "a" ($#r1_hidden :::"="::: ) (Num 1)) (Num 1) if (Bool "(" (Bool "a" ($#r1_hidden :::"="::: ) (Num 2)) & (Bool "b" ($#r1_hidden :::"="::: ) (Num 2)) ")" ) ; end; :: deftheorem defines :::"-"::: MOD_2:def 12 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k10_mod_2 :::"-"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set ($#k10_mod_2 :::"-"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Num 2)) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Num 2))) "implies" (Bool (Set ($#k10_mod_2 :::"-"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" )); :: deftheorem defines :::"+"::: MOD_2:def 13 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "a")) ($#k11_mod_2 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "a")) ($#k11_mod_2 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set (Set (Var "a")) ($#k11_mod_2 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Num 2)) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Num 2))) "implies" (Bool (Set (Set (Var "a")) ($#k11_mod_2 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set (Set (Var "a")) ($#k11_mod_2 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Num 2))) "implies" (Bool (Set (Set (Var "a")) ($#k11_mod_2 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" )); :: deftheorem defines :::"*"::: MOD_2:def 14 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "a")) ($#k12_mod_2 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "a")) ($#k12_mod_2 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set (Set (Var "a")) ($#k12_mod_2 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set (Set (Var "a")) ($#k12_mod_2 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Num 2))) "implies" (Bool (Set (Set (Var "a")) ($#k12_mod_2 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" )); definitionfunc :::"add3"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) means :: MOD_2:def 15 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k11_mod_2 :::"+"::: ) (Set (Var "b"))))); func :::"mult3"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) means :: MOD_2:def 16 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_mod_2 :::"*"::: ) (Set (Var "b"))))); func :::"compl3"::: -> ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) means :: MOD_2:def 17 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k10_mod_2 :::"-"::: ) (Set (Var "a"))))); func :::"unit3"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) equals :: MOD_2:def 18 (Num 1); func :::"zero3"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) equals :: MOD_2:def 19 (Set ($#k6_numbers :::"0"::: ) ); end; :: deftheorem defines :::"add3"::: MOD_2:def 15 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k13_mod_2 :::"add3"::: ) )) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k11_mod_2 :::"+"::: ) (Set (Var "b"))))) ")" )); :: deftheorem defines :::"mult3"::: MOD_2:def 16 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k14_mod_2 :::"mult3"::: ) )) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_mod_2 :::"*"::: ) (Set (Var "b"))))) ")" )); :: deftheorem defines :::"compl3"::: MOD_2:def 17 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k15_mod_2 :::"compl3"::: ) )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k10_mod_2 :::"-"::: ) (Set (Var "a"))))) ")" )); :: deftheorem defines :::"unit3"::: MOD_2:def 18 : (Bool (Set ($#k16_mod_2 :::"unit3"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)); :: deftheorem defines :::"zero3"::: MOD_2:def 19 : (Bool (Set ($#k17_mod_2 :::"zero3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); definitionfunc :::"Z_3"::: -> ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) equals :: MOD_2:def 20 (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "," (Set ($#k13_mod_2 :::"add3"::: ) ) "," (Set ($#k14_mod_2 :::"mult3"::: ) ) "," (Set ($#k16_mod_2 :::"unit3"::: ) ) "," (Set ($#k17_mod_2 :::"zero3"::: ) ) "#)" ); end; :: deftheorem defines :::"Z_3"::: MOD_2:def 20 : (Bool (Set ($#k18_mod_2 :::"Z_3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "," (Set ($#k13_mod_2 :::"add3"::: ) ) "," (Set ($#k14_mod_2 :::"mult3"::: ) ) "," (Set ($#k16_mod_2 :::"unit3"::: ) ) "," (Set ($#k17_mod_2 :::"zero3"::: ) ) "#)" )); registration cluster (Set ($#k18_mod_2 :::"Z_3"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ; end; registration cluster (Set ($#k18_mod_2 :::"Z_3"::: ) ) -> ($#v36_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ; end; theorem :: MOD_2:22 (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k18_mod_2 :::"Z_3"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set ($#k18_mod_2 :::"Z_3"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k18_mod_2 :::"Z_3"::: ) )) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) )) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set ($#k18_mod_2 :::"Z_3"::: ) )) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) )) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set ($#k18_mod_2 :::"Z_3"::: ) )) ($#r1_funct_2 :::"="::: ) (Set ($#k13_mod_2 :::"add3"::: ) )) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set ($#k18_mod_2 :::"Z_3"::: ) )) ($#r1_funct_2 :::"="::: ) (Set ($#k14_mod_2 :::"mult3"::: ) )) ")" ) ; registration cluster (Set ($#k18_mod_2 :::"Z_3"::: ) ) -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; theorem :: MOD_2:23 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set ($#k18_mod_2 :::"Z_3"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k11_mod_2 :::"+"::: ) (Set (Var "Y")))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k12_mod_2 :::"*"::: ) (Set (Var "Y")))) & (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k10_mod_2 :::"-"::: ) (Set (Var "X")))) ")" ))) ; theorem :: MOD_2:24 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set ($#k18_mod_2 :::"Z_3"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set (Var "z")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k11_mod_2 :::"+"::: ) (Set (Var "Y")) ")" ) ($#k11_mod_2 :::"+"::: ) (Set (Var "Z")))) & (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k11_mod_2 :::"+"::: ) (Set "(" (Set (Var "Y")) ($#k11_mod_2 :::"+"::: ) (Set (Var "Z")) ")" ))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k12_mod_2 :::"*"::: ) (Set (Var "Y")) ")" ) ($#k12_mod_2 :::"*"::: ) (Set (Var "Z")))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k12_mod_2 :::"*"::: ) (Set "(" (Set (Var "Y")) ($#k12_mod_2 :::"*"::: ) (Set (Var "Z")) ")" ))) ")" ))) ; theorem :: MOD_2:25 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k11_mod_2 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k11_mod_2 :::"+"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k11_mod_2 :::"+"::: ) (Set (Var "y")) ")" ) ($#k11_mod_2 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_mod_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k11_mod_2 :::"+"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k11_mod_2 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "x")) ($#k11_mod_2 :::"+"::: ) (Set "(" ($#k10_mod_2 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "x")) ($#k12_mod_2 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k12_mod_2 :::"*"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k12_mod_2 :::"*"::: ) (Set (Var "y")) ")" ) ($#k12_mod_2 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k12_mod_2 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k12_mod_2 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "b")) ($#k12_mod_2 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "implies" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ) "st" (Bool (Set (Set (Var "x")) ($#k12_mod_2 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Set (Var "x")) ($#k12_mod_2 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k11_mod_2 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k12_mod_2 :::"*"::: ) (Set (Var "y")) ")" ) ($#k11_mod_2 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k12_mod_2 :::"*"::: ) (Set (Var "z")) ")" ))) ")" )) ; theorem :: MOD_2:26 (Bool "for" (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "F")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F"))))) "implies" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F")) "st" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "F"))))) ")" & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F"))) ($#r1_hidden :::"<>"::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) ")" ) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#l6_algstr_0 :::"Field":::))) ; theorem :: MOD_2:27 (Bool (Set ($#k18_mod_2 :::"Z_3"::: ) ) "is" ($#v12_vectsp_1 :::"Fanoian"::: ) ($#l6_algstr_0 :::"Field":::)) ; registration cluster (Set ($#k18_mod_2 :::"Z_3"::: ) ) -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v12_vectsp_1 :::"Fanoian"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; theorem :: MOD_2:28 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "D9")) "st" (Bool (Bool (Set (Var "D")) ($#r2_hidden :::"in"::: ) (Set (Var "UN"))) & (Bool (Set (Var "D9")) ($#r2_hidden :::"in"::: ) (Set (Var "UN")))) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "UN")))))) ; theorem :: MOD_2:29 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k18_mod_2 :::"Z_3"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "UN"))) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set ($#k18_mod_2 :::"Z_3"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "UN"))) & (Bool (Set ($#k5_vectsp_1 :::"comp"::: ) (Set ($#k18_mod_2 :::"Z_3"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "UN"))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k18_mod_2 :::"Z_3"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "UN"))) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set ($#k18_mod_2 :::"Z_3"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "UN"))) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set ($#k18_mod_2 :::"Z_3"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "UN"))) ")" )) ;