:: GROUP_7 semantic presentation begin definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"multMagma-yielding"::: means :: GROUP_7:def 1 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool (Set (Var "y")) "is" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) )); end; :: deftheorem defines :::"multMagma-yielding"::: GROUP_7:def 1 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_group_7 :::"multMagma-yielding"::: ) ) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "y")) "is" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) )) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_group_7 :::"multMagma-yielding"::: ) -> ($#v2_pralg_1 :::"1-sorted-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_group_7 :::"multMagma-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_group_7 :::"multMagma-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; mode multMagma-Family of "I" is ($#v1_group_7 :::"multMagma-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" "I"; end; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); :: original: :::"."::: redefine func "F" :::"."::: "i" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); cluster (Set ($#k12_pralg_1 :::"Carrier"::: ) "F") -> bbbadV2_RELAT_1() ; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); func :::"product"::: "F" -> ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"multMagma"::: ) means :: GROUP_7:def 2 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) "F" ")" ))) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) "F" ")" )) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool "ex" (Set (Var "Fi")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "Fi")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "Fi"))) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ")" )) ")" )))) ")" ) ")" ); end; :: deftheorem defines :::"product"::: GROUP_7:def 2 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b3")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_group_7 :::"product"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "F")) ")" ))) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "F")) ")" )) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "ex" (Set (Var "Fi")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "Fi")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b3"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "Fi"))) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ")" )) ")" )))) ")" ) ")" ) ")" )))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); cluster (Set ($#k2_group_7 :::"product"::: ) "F") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_monoid_0 :::"constituted-Functions"::: ) ; end; theorem :: GROUP_7:1 (Bool "for" (Set (Var "I")) "," (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "q")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); attr "F" is :::"Group-like"::: means :: GROUP_7:def 3 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool "ex" (Set (Var "Fi")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool (Set (Var "Fi")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))); attr "F" is :::"associative"::: means :: GROUP_7:def 4 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool "ex" (Set (Var "Fi")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool (Set (Var "Fi")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))); attr "F" is :::"commutative"::: means :: GROUP_7:def 5 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool "ex" (Set (Var "Fi")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool (Set (Var "Fi")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))); end; :: deftheorem defines :::"Group-like"::: GROUP_7:def 3 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_group_7 :::"Group-like"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "ex" (Set (Var "Fi")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool (Set (Var "Fi")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))) ")" ))); :: deftheorem defines :::"associative"::: GROUP_7:def 4 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_group_7 :::"associative"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "ex" (Set (Var "Fi")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool (Set (Var "Fi")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))) ")" ))); :: deftheorem defines :::"commutative"::: GROUP_7:def 5 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_group_7 :::"commutative"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "ex" (Set (Var "Fi")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool (Set (Var "Fi")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))) ")" ))); definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); redefine attr "F" is :::"Group-like"::: means :: GROUP_7:def 6 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "I" "holds" (Bool (Set "F" ($#k1_group_7 :::"."::: ) (Set (Var "i"))) "is" ($#v2_group_1 :::"Group-like"::: ) )); redefine attr "F" is :::"associative"::: means :: GROUP_7:def 7 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "I" "holds" (Bool (Set "F" ($#k1_group_7 :::"."::: ) (Set (Var "i"))) "is" ($#v3_group_1 :::"associative"::: ) )); redefine attr "F" is :::"commutative"::: means :: GROUP_7:def 8 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "I" "holds" (Bool (Set "F" ($#k1_group_7 :::"."::: ) (Set (Var "i"))) "is" ($#v5_group_1 :::"commutative"::: ) )); end; :: deftheorem defines :::"Group-like"::: GROUP_7:def 6 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_group_7 :::"Group-like"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "i"))) "is" ($#v2_group_1 :::"Group-like"::: ) )) ")" ))); :: deftheorem defines :::"associative"::: GROUP_7:def 7 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_group_7 :::"associative"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "i"))) "is" ($#v3_group_1 :::"associative"::: ) )) ")" ))); :: deftheorem defines :::"commutative"::: GROUP_7:def 8 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_group_7 :::"commutative"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "i"))) "is" ($#v5_group_1 :::"commutative"::: ) )) ")" ))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v2_pralg_1 :::"1-sorted-yielding"::: ) ($#v1_group_7 :::"multMagma-yielding"::: ) ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#v4_group_7 :::"commutative"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_group_7 :::"Group-like"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); cluster (Set ($#k2_group_7 :::"product"::: ) "F") -> ($#v15_algstr_0 :::"strict"::: ) ($#v2_group_1 :::"Group-like"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); cluster (Set ($#k2_group_7 :::"product"::: ) "F") -> ($#v15_algstr_0 :::"strict"::: ) ($#v3_group_1 :::"associative"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#v4_group_7 :::"commutative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); cluster (Set ($#k2_group_7 :::"product"::: ) "F") -> ($#v15_algstr_0 :::"strict"::: ) ($#v5_group_1 :::"commutative"::: ) ; end; theorem :: GROUP_7:2 (Bool "for" (Set (Var "I")) "," (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k2_group_7 :::"product"::: ) (Set (Var "F"))) "is" ($#v2_group_1 :::"Group-like"::: ) )) "holds" (Bool (Set (Var "G")) "is" ($#v2_group_1 :::"Group-like"::: ) )))) ; theorem :: GROUP_7:3 (Bool "for" (Set (Var "I")) "," (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k2_group_7 :::"product"::: ) (Set (Var "F"))) "is" ($#v3_group_1 :::"associative"::: ) )) "holds" (Bool (Set (Var "G")) "is" ($#v3_group_1 :::"associative"::: ) )))) ; theorem :: GROUP_7:4 (Bool "for" (Set (Var "I")) "," (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k2_group_7 :::"product"::: ) (Set (Var "F"))) "is" ($#v5_group_1 :::"commutative"::: ) )) "holds" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) )))) ; theorem :: GROUP_7:5 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#v2_group_7 :::"Group-like"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) ")" )) ")" )) "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" )))))) ; theorem :: GROUP_7:6 (Bool "for" (Set (Var "I")) "," (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "F")) "being" ($#v2_group_7 :::"Group-like"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))))) ; theorem :: GROUP_7:7 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::)(Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k2_group_1 :::"""::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ))) ")" )) "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_group_1 :::"""::: ) ))))))) ; theorem :: GROUP_7:8 (Bool "for" (Set (Var "I")) "," (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "F")) "being" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_group_1 :::"""::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k2_group_1 :::"""::: ) )))))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); func :::"sum"::: "F" -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set ($#k2_group_7 :::"product"::: ) "F") means :: GROUP_7:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) "F" ")" ))(Bool "ex" (Set (Var "J")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "I"(Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) "F" ")" ))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set (Var "J")))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) ")" )) ")" ) ")" )))) ")" )); end; :: deftheorem defines :::"sum"::: GROUP_7:def 9 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b3")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set ($#k2_group_7 :::"product"::: ) (Set (Var "F"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_7 :::"sum"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3")))) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "F")) ")" ))(Bool "ex" (Set (Var "J")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I"))(Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set (Var "J")))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) ")" )) ")" ) ")" )))) ")" )) ")" )))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); let "f", "g" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_group_7 :::"sum"::: ) (Set (Const "F")) ")" ); cluster (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set "(" ($#k3_group_7 :::"sum"::: ) "F" ")" )) ($#k1_binop_1 :::"."::: ) "(" "f" "," "g" ")" ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: GROUP_7:9 (Bool "for" (Set (Var "I")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k2_group_7 :::"product"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_group_7 :::"sum"::: ) (Set (Var "F")))))) ; begin theorem :: GROUP_7:10 (Bool "for" (Set (Var "G1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "G1")) ($#k9_finseq_1 :::"*>"::: ) ) "is" ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ))) ; registrationlet "G1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k5_finseq_1 :::"<*"::: ) "G1" ($#k5_finseq_1 :::"*>"::: ) ) -> (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "G1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k5_finseq_1 :::"<*"::: ) "G1" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v1_partfun1 :::"total"::: ) ($#v1_group_7 :::"multMagma-yielding"::: ) ; end; theorem :: GROUP_7:11 (Bool "for" (Set (Var "G1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "G1")) ($#k9_finseq_1 :::"*>"::: ) ) "is" ($#v2_group_7 :::"Group-like"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ))) ; registrationlet "G1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k5_finseq_1 :::"<*"::: ) "G1" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v2_group_7 :::"Group-like"::: ) ; end; theorem :: GROUP_7:12 (Bool "for" (Set (Var "G1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "G1")) ($#k9_finseq_1 :::"*>"::: ) ) "is" ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ))) ; registrationlet "G1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k5_finseq_1 :::"<*"::: ) "G1" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v3_group_7 :::"associative"::: ) ; end; theorem :: GROUP_7:13 (Bool "for" (Set (Var "G1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "G1")) ($#k9_finseq_1 :::"*>"::: ) ) "is" ($#v4_group_7 :::"commutative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ))) ; registrationlet "G1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k5_finseq_1 :::"<*"::: ) "G1" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v4_group_7 :::"commutative"::: ) ; end; theorem :: GROUP_7:14 (Bool "for" (Set (Var "G1")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "G1")) ($#k9_finseq_1 :::"*>"::: ) ) "is" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ))) ; theorem :: GROUP_7:15 (Bool "for" (Set (Var "G1")) "being" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "G1")) ($#k9_finseq_1 :::"*>"::: ) ) "is" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#v4_group_7 :::"commutative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ))) ; registrationlet "G1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) "G1" ($#k9_finseq_1 :::"*>"::: ) ) ")" )); end; registrationlet "G1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) "G1" ($#k9_finseq_1 :::"*>"::: ) ) ")" )); end; definitionlet "G1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G1")); :: original: :::"<*"::: redefine func :::"<*":::"x":::"*>"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) "G1" ($#k9_finseq_1 :::"*>"::: ) ) ")" ); end; theorem :: GROUP_7:16 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) ($#k10_finseq_1 :::"*>"::: ) ) "is" ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k2_tarski :::"{"::: ) (Num 1) "," (Num 2) ($#k2_tarski :::"}"::: ) ))) ; registrationlet "G1", "G2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k10_finseq_1 :::"<*"::: ) "G1" "," "G2" ($#k10_finseq_1 :::"*>"::: ) ) -> (Set ($#k2_tarski :::"{"::: ) (Num 1) "," (Num 2) ($#k2_tarski :::"}"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "G1", "G2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k10_finseq_1 :::"<*"::: ) "G1" "," "G2" ($#k10_finseq_1 :::"*>"::: ) ) -> ($#v1_partfun1 :::"total"::: ) ($#v1_group_7 :::"multMagma-yielding"::: ) ; end; theorem :: GROUP_7:17 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) ($#k10_finseq_1 :::"*>"::: ) ) "is" ($#v2_group_7 :::"Group-like"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k2_tarski :::"{"::: ) (Num 1) "," (Num 2) ($#k2_tarski :::"}"::: ) ))) ; registrationlet "G1", "G2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k10_finseq_1 :::"<*"::: ) "G1" "," "G2" ($#k10_finseq_1 :::"*>"::: ) ) -> ($#v2_group_7 :::"Group-like"::: ) ; end; theorem :: GROUP_7:18 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) ($#k10_finseq_1 :::"*>"::: ) ) "is" ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k2_tarski :::"{"::: ) (Num 1) "," (Num 2) ($#k2_tarski :::"}"::: ) ))) ; registrationlet "G1", "G2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k10_finseq_1 :::"<*"::: ) "G1" "," "G2" ($#k10_finseq_1 :::"*>"::: ) ) -> ($#v3_group_7 :::"associative"::: ) ; end; theorem :: GROUP_7:19 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) ($#k10_finseq_1 :::"*>"::: ) ) "is" ($#v4_group_7 :::"commutative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k2_tarski :::"{"::: ) (Num 1) "," (Num 2) ($#k2_tarski :::"}"::: ) ))) ; registrationlet "G1", "G2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k10_finseq_1 :::"<*"::: ) "G1" "," "G2" ($#k10_finseq_1 :::"*>"::: ) ) -> ($#v4_group_7 :::"commutative"::: ) ; end; theorem :: GROUP_7:20 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) ($#k10_finseq_1 :::"*>"::: ) ) "is" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k2_tarski :::"{"::: ) (Num 1) "," (Num 2) ($#k2_tarski :::"}"::: ) ))) ; theorem :: GROUP_7:21 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) ($#k10_finseq_1 :::"*>"::: ) ) "is" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#v4_group_7 :::"commutative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k2_tarski :::"{"::: ) (Num 1) "," (Num 2) ($#k2_tarski :::"}"::: ) ))) ; registrationlet "G1", "G2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "G1" "," "G2" ($#k10_finseq_1 :::"*>"::: ) ) ")" )); end; registrationlet "G1", "G2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "G1" "," "G2" ($#k10_finseq_1 :::"*>"::: ) ) ")" )); end; definitionlet "G1", "G2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G1")); let "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G2")); :: original: :::"<*"::: redefine func :::"<*":::"x" "," "y":::"*>"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "G1" "," "G2" ($#k10_finseq_1 :::"*>"::: ) ) ")" ); end; theorem :: GROUP_7:22 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) ($#k11_finseq_1 :::"*>"::: ) ) "is" ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k1_enumset1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) ($#k1_enumset1 :::"}"::: ) ))) ; registrationlet "G1", "G2", "G3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k11_finseq_1 :::"<*"::: ) "G1" "," "G2" "," "G3" ($#k11_finseq_1 :::"*>"::: ) ) -> (Set ($#k1_enumset1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) ($#k1_enumset1 :::"}"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "G1", "G2", "G3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k11_finseq_1 :::"<*"::: ) "G1" "," "G2" "," "G3" ($#k11_finseq_1 :::"*>"::: ) ) -> ($#v1_partfun1 :::"total"::: ) ($#v1_group_7 :::"multMagma-yielding"::: ) ; end; theorem :: GROUP_7:23 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) ($#k11_finseq_1 :::"*>"::: ) ) "is" ($#v2_group_7 :::"Group-like"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k1_enumset1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) ($#k1_enumset1 :::"}"::: ) ))) ; registrationlet "G1", "G2", "G3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k11_finseq_1 :::"<*"::: ) "G1" "," "G2" "," "G3" ($#k11_finseq_1 :::"*>"::: ) ) -> ($#v2_group_7 :::"Group-like"::: ) ; end; theorem :: GROUP_7:24 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) ($#k11_finseq_1 :::"*>"::: ) ) "is" ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k1_enumset1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) ($#k1_enumset1 :::"}"::: ) ))) ; registrationlet "G1", "G2", "G3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k11_finseq_1 :::"<*"::: ) "G1" "," "G2" "," "G3" ($#k11_finseq_1 :::"*>"::: ) ) -> ($#v3_group_7 :::"associative"::: ) ; end; theorem :: GROUP_7:25 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) ($#k11_finseq_1 :::"*>"::: ) ) "is" ($#v4_group_7 :::"commutative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k1_enumset1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) ($#k1_enumset1 :::"}"::: ) ))) ; registrationlet "G1", "G2", "G3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k11_finseq_1 :::"<*"::: ) "G1" "," "G2" "," "G3" ($#k11_finseq_1 :::"*>"::: ) ) -> ($#v4_group_7 :::"commutative"::: ) ; end; theorem :: GROUP_7:26 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) ($#k11_finseq_1 :::"*>"::: ) ) "is" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k1_enumset1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: GROUP_7:27 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) ($#k11_finseq_1 :::"*>"::: ) ) "is" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#v4_group_7 :::"commutative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k1_enumset1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) ($#k1_enumset1 :::"}"::: ) ))) ; registrationlet "G1", "G2", "G3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set ($#k11_finseq_1 :::"<*"::: ) "G1" "," "G2" "," "G3" ($#k11_finseq_1 :::"*>"::: ) ) ")" )); end; registrationlet "G1", "G2", "G3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k11_finseq_1 :::"<*"::: ) "G1" "," "G2" "," "G3" ($#k11_finseq_1 :::"*>"::: ) ) ")" )); end; definitionlet "G1", "G2", "G3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G1")); let "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G2")); let "z" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G3")); :: original: :::"<*"::: redefine func :::"<*":::"x" "," "y" "," "z":::"*>"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k11_finseq_1 :::"<*"::: ) "G1" "," "G2" "," "G3" ($#k11_finseq_1 :::"*>"::: ) ) ")" ); end; theorem :: GROUP_7:28 (Bool "for" (Set (Var "G1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G1")) "holds" (Bool (Set (Set ($#k4_group_7 :::"<*"::: ) (Set (Var "x1")) ($#k4_group_7 :::"*>"::: ) ) ($#k6_algstr_0 :::"*"::: ) (Set ($#k4_group_7 :::"<*"::: ) (Set (Var "x2")) ($#k4_group_7 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_group_7 :::"<*"::: ) (Set "(" (Set (Var "x1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k4_group_7 :::"*>"::: ) )))) ; theorem :: GROUP_7:29 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G2")) "holds" (Bool (Set (Set ($#k5_group_7 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k5_group_7 :::"*>"::: ) ) ($#k6_algstr_0 :::"*"::: ) (Set ($#k5_group_7 :::"<*"::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k5_group_7 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_group_7 :::"<*"::: ) (Set "(" (Set (Var "x1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "y1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y2")) ")" ) ($#k5_group_7 :::"*>"::: ) ))))) ; theorem :: GROUP_7:30 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G2")) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G3")) "holds" (Bool (Set (Set ($#k6_group_7 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) ($#k6_group_7 :::"*>"::: ) ) ($#k6_algstr_0 :::"*"::: ) (Set ($#k6_group_7 :::"<*"::: ) (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "z2")) ($#k6_group_7 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_group_7 :::"<*"::: ) (Set "(" (Set (Var "x1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "y1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y2")) ")" ) "," (Set "(" (Set (Var "z1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z2")) ")" ) ($#k6_group_7 :::"*>"::: ) )))))) ; theorem :: GROUP_7:31 (Bool "for" (Set (Var "G1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "G1")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_group_7 :::"<*"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G1")) ")" ) ($#k4_group_7 :::"*>"::: ) ))) ; theorem :: GROUP_7:32 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) ($#k10_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_group_7 :::"<*"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G1")) ")" ) "," (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G2")) ")" ) ($#k5_group_7 :::"*>"::: ) ))) ; theorem :: GROUP_7:33 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) ($#k11_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_group_7 :::"<*"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G1")) ")" ) "," (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G2")) ")" ) "," (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G3")) ")" ) ($#k6_group_7 :::"*>"::: ) ))) ; theorem :: GROUP_7:34 (Bool "for" (Set (Var "G1")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G1")) "holds" (Bool (Set (Set ($#k4_group_7 :::"<*"::: ) (Set (Var "x")) ($#k4_group_7 :::"*>"::: ) ) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_group_7 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k2_group_1 :::"""::: ) ")" ) ($#k4_group_7 :::"*>"::: ) )))) ; theorem :: GROUP_7:35 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G2")) "holds" (Bool (Set (Set ($#k5_group_7 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k5_group_7 :::"*>"::: ) ) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_group_7 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set "(" (Set (Var "y")) ($#k2_group_1 :::"""::: ) ")" ) ($#k5_group_7 :::"*>"::: ) ))))) ; theorem :: GROUP_7:36 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G2")) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G3")) "holds" (Bool (Set (Set ($#k6_group_7 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k6_group_7 :::"*>"::: ) ) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_group_7 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set "(" (Set (Var "y")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_group_7 :::"*>"::: ) )))))) ; theorem :: GROUP_7:37 (Bool "for" (Set (Var "G1")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "G1")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G1")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_group_7 :::"<*"::: ) (Set (Var "x")) ($#k4_group_7 :::"*>"::: ) )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G1")) "," (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "G1")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )))) ; theorem :: GROUP_7:38 (Bool "for" (Set (Var "G1")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G1")) "," (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "G1")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G1")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_group_7 :::"<*"::: ) (Set (Var "x")) ($#k4_group_7 :::"*>"::: ) )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v3_funct_2 :::"bijective"::: ) ))) ; theorem :: GROUP_7:39 (Bool "for" (Set (Var "G1")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set (Var "G1")) "," (Set ($#k2_group_7 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "G1")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_group_6 :::"are_isomorphic"::: ) )) ;