:: GROUP_12 semantic presentation begin registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_group_7 :::"Group-like"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); cluster (Set "F" ($#k1_funct_1 :::"."::: ) "i") -> ($#v2_group_1 :::"Group-like"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); cluster (Set "F" ($#k1_funct_1 :::"."::: ) "i") -> ($#v3_group_1 :::"associative"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v4_group_7 :::"commutative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); cluster (Set "F" ($#k1_funct_1 :::"."::: ) "i") -> ($#v5_group_1 :::"commutative"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; theorem :: GROUP_12:1 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "i")) ")" ) "holds" (Bool "(" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "I"))) & (Bool (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set "(" (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "j")) ")" ))) ")" ) ")" ) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "g")) ")" )) ")" )))))) ; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); func :::"ProjSet"::: "(" "F" "," "i" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) "F" ")" ) means :: GROUP_12:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" "F" ($#k1_group_7 :::"."::: ) "i" ")" ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) "F" ")" ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "g")) ")" ))) ")" )); end; :: deftheorem defines :::"ProjSet"::: GROUP_12:def 1 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_12 :::"ProjSet"::: ) "(" (Set (Var "F")) "," (Set (Var "i")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "g")) ")" ))) ")" )) ")" ))))); registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); cluster (Set ($#k1_group_12 :::"ProjSet"::: ) "(" "F" "," "i" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: GROUP_12:2 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "x0")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set ($#k1_group_12 :::"ProjSet"::: ) "(" (Set (Var "F")) "," (Set (Var "i")) ")" )) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"Function":::)(Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x0"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "I"))) & (Bool (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set "(" (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "j")) ")" ))) ")" ) ")" ))) ")" ))))) ; theorem :: GROUP_12:3 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "g1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "z1")) ")" )) & (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "z2")) ")" ))) "holds" (Bool (Set (Set (Var "g1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "z1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z2")) ")" ) ")" ))))))) ; theorem :: GROUP_12:4 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) (Bool "for" (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "g1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "z1")) ")" ))) "holds" (Bool (Set (Set (Var "g1")) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "z1")) ($#k2_group_1 :::"""::: ) ")" ) ")" ))))))) ; theorem :: GROUP_12:5 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_group_12 :::"ProjSet"::: ) "(" (Set (Var "F")) "," (Set (Var "i")) ")" )) & (Bool (Set (Var "g2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_group_12 :::"ProjSet"::: ) "(" (Set (Var "F")) "," (Set (Var "i")) ")" ))) "holds" (Bool (Set (Set (Var "g1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_group_12 :::"ProjSet"::: ) "(" (Set (Var "F")) "," (Set (Var "i")) ")" )))))) ; theorem :: GROUP_12:6 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_group_12 :::"ProjSet"::: ) "(" (Set (Var "F")) "," (Set (Var "i")) ")" ))) "holds" (Bool (Set (Set (Var "g")) ($#k2_group_1 :::"""::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_group_12 :::"ProjSet"::: ) "(" (Set (Var "F")) "," (Set (Var "i")) ")" )))))) ; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); func :::"ProjGroup"::: "(" "F" "," "i" ")" -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set ($#k2_group_7 :::"product"::: ) "F") means :: GROUP_12:def 2 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_group_12 :::"ProjSet"::: ) "(" "F" "," "i" ")" )); end; :: deftheorem defines :::"ProjGroup"::: GROUP_12:def 2 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "b4")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set ($#k2_group_7 :::"product"::: ) (Set (Var "F"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_group_12 :::"ProjGroup"::: ) "(" (Set (Var "F")) "," (Set (Var "i")) ")" )) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_12 :::"ProjSet"::: ) "(" (Set (Var "F")) "," (Set (Var "i")) ")" )) ")" ))))); definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); func :::"1ProdHom"::: "(" "F" "," "i" ")" -> ($#m1_subset_1 :::"Homomorphism":::) "of" (Set "(" "F" ($#k1_group_7 :::"."::: ) "i" ")" ) "," (Set "(" ($#k2_group_12 :::"ProjGroup"::: ) "(" "F" "," "i" ")" ")" ) means :: GROUP_12:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" "F" ($#k1_group_7 :::"."::: ) "i" ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) "F" ")" ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "x")) ")" ))); end; :: deftheorem defines :::"1ProdHom"::: GROUP_12:def 3 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set "(" (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" ($#k2_group_12 :::"ProjGroup"::: ) "(" (Set (Var "F")) "," (Set (Var "i")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_12 :::"1ProdHom"::: ) "(" (Set (Var "F")) "," (Set (Var "i")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "i")) ")" ) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ))) ")" ))))); registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); cluster (Set ($#k3_group_12 :::"1ProdHom"::: ) "(" "F" "," "i" ")" ) -> ($#v3_funct_2 :::"bijective"::: ) ; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); cluster (Set ($#k2_group_12 :::"ProjGroup"::: ) "(" "F" "," "i" ")" ) -> ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ; end; theorem :: GROUP_12:7 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j"))) & (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set ($#k2_group_12 :::"ProjGroup"::: ) "(" (Set (Var "F")) "," (Set (Var "i")) ")" )) & (Bool (Set (Var "y")) ($#r1_struct_0 :::"in"::: ) (Set ($#k2_group_12 :::"ProjGroup"::: ) "(" (Set (Var "F")) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")))))))) ; theorem :: GROUP_12:8 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "GJ")) "being" ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "J"))) & (Bool (Set (Var "J")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "GJ")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "J"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) (Bool "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "J"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s"))))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_struct_0 :::"in"::: ) (Set ($#k2_group_12 :::"ProjGroup"::: ) "(" (Set (Var "F")) "," (Set (Var "k")) ")" )) ")" ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "s"))))) "holds" (Bool (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "J"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "GJ")))))))))) ; theorem :: GROUP_12:9 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) (Bool "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_struct_0 :::"in"::: ) (Set ($#k2_group_12 :::"ProjGroup"::: ) "(" (Set (Var "F")) "," (Set (Var "k")) ")" )) ")" ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "s"))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "ex" (Set (Var "si")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) "st" (Bool "(" (Bool (Set (Var "si")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "si")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ))))))) ; theorem :: GROUP_12:10 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_struct_0 :::"in"::: ) (Set ($#k2_group_12 :::"ProjGroup"::: ) "(" (Set (Var "F")) "," (Set (Var "k")) ")" )) ")" ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "s")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_struct_0 :::"in"::: ) (Set ($#k2_group_12 :::"ProjGroup"::: ) "(" (Set (Var "F")) "," (Set (Var "k")) ")" )) ")" ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "t"))))) "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "t"))))))) ; theorem :: GROUP_12:11 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) (Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_struct_0 :::"in"::: ) (Set ($#k2_group_12 :::"ProjGroup"::: ) "(" (Set (Var "F")) "," (Set (Var "k")) ")" )) ")" ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "s")))) ")" ))))) ; theorem :: GROUP_12:12 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F")) "being" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "i"))) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "k")))) ")" ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "s")))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "k")))) ")" ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "k")))) ")" ) & (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "t"))))) "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) ")" )) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) "," (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) (Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "k")))) ")" ) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "s")))) ")" )) ")" ) ")" ))))) ; theorem :: GROUP_12:13 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#v2_group_7 :::"Group-like"::: ) ($#v3_group_7 :::"associative"::: ) ($#v4_group_7 :::"commutative"::: ) ($#m1_hidden :::"multMagma-Family":::) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) "st" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k2_group_12 :::"ProjGroup"::: ) "(" (Set (Var "G")) "," (Set (Var "k")) ")" )) ")" )) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) "," (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "G")) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "F")) ")" ) (Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set (Var "G")) ")" ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "F")) ($#k1_group_7 :::"."::: ) (Set (Var "k")))) ")" ) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "s")))) ")" )) ")" ) ")" )))) ;