:: GROUP_6  semantic presentation begin  
theorem :: GROUP_6:1 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))  ")" ))) ; 
 definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "A" be    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); :: original: :::"Subgroup"::: redefine mode  :::"Subgroup":::  "of" "A" ->    ($#m1_group_2 :::"Subgroup"::: )   "of" "G"; end; registrationlet "G" be   ($#l3_algstr_0 :::"Group":::); 
cluster (Set   ($#k6_group_2 :::"(1)."::: )  "G") ->   ($#v1_group_3 :::"normal"::: )   ; 

cluster (Set   ($#k7_group_2 :::"(Omega)."::: )  "G") ->   ($#v1_group_3 :::"normal"::: )   ; 
end; 












































theorem :: GROUP_6:2 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "A")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_group_6 :::"Subgroup"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k13_group_2 :::"*"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k13_group_2 :::"*"::: )  (Set (Var "X")))) & (Bool (Set (Set (Var "X"))  ($#k14_group_2 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k14_group_2 :::"*"::: )  (Set (Var "a"))))  ")" )))))) ; 
 
theorem :: GROUP_6:3 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "A")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_group_6 :::"Subgroup"::: )   "of" (Set (Var "A")) "holds"  (Bool (Set (Set (Var "X"))  ($#k10_group_2 :::"/\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k10_group_2 :::"/\"::: )  (Set (Var "Y"))))))) ; 
 
theorem :: GROUP_6:4 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k2_group_1 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k2_group_3 :::"|^"::: )  (Set  "(" (Set (Var "a"))  ($#k2_group_1 :::"""::: )  ")" ))) & (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k6_algstr_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k2_group_1 :::"""::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k2_group_3 :::"|^"::: )  (Set  "(" (Set (Var "a"))  ($#k2_group_1 :::"""::: )  ")" )))  ")" ))) ; 
 
theorem :: GROUP_6:5 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "A")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k13_group_2 :::"*"::: )  (Set (Var "A")) ")" )  ($#k11_group_2 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k13_group_2 :::"*"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "a"))  ($#k4_group_2 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k7_group_4 :::"*"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k13_group_2 :::"*"::: )  (Set (Var "A")))) & (Bool (Set (Set  "(" (Set (Var "A"))  ($#k7_group_4 :::"*"::: )  (Set (Var "A")) ")" )  ($#k5_group_2 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k14_group_2 :::"*"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "A"))  ($#k12_group_2 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k14_group_2 :::"*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k14_group_2 :::"*"::: )  (Set (Var "a"))))  ")" )))) ; 
 
theorem :: GROUP_6:6 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "A1"))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) where a, b "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool verum)  "}"  )) "holds"  (Bool (Set (Set (Var "G"))  ($#k9_group_5 :::"`"::: )  )  ($#r1_group_2 :::"="::: )  (Set   ($#k5_group_4 :::"gr"::: )  (Set (Var "A1")))))) ; 
 
theorem :: GROUP_6:7 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "B")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Set (Var "G"))  ($#k9_group_5 :::"`"::: )  ) "is"    ($#m1_group_6 :::"Subgroup"::: )   "of" (Set (Var "B"))) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set  ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) )  ($#r1_struct_0 :::"in"::: )  (Set (Var "B"))))  ")" ))) ; 
 
theorem :: GROUP_6:8 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "B")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "N")) "is"    ($#m1_group_6 :::"Subgroup"::: )   "of" (Set (Var "B")))) "holds"  (Bool (Set (Var "N")) "is"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_6 :::"Subgroup"::: )   "of" (Set (Var "B")))))) ; 
 definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "B" be    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); let "M" be   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); assume 
(Bool (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "M"))) "," (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Const "M"))) "#)" ) "is"    ($#m1_group_6 :::"Subgroup"::: )   "of" (Set (Const "B")))
 ; func  "(" "B" "," "M" ")"  :::"`*`":::  ->   ($#v15_algstr_0 :::"strict"::: )     ($#v1_group_3 :::"normal"::: )     ($#m1_group_6 :::"Subgroup"::: )   "of" "B" equals :: GROUP_6:def 1 (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "M") "," (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" "M") "#)" ); end; 








:: deftheorem    defines :::"`*`"::: GROUP_6:def 1 :  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "B")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "M")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "M"))) "," (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "M"))) "#)" ) "is"    ($#m1_group_6 :::"Subgroup"::: )   "of" (Set (Var "B")))) "holds"  (Bool (Set  "(" (Set (Var "B")) "," (Set (Var "M")) ")"   ($#k1_group_6 :::"`*`"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "M"))) "," (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "M"))) "#)" ))))); 
 
theorem :: GROUP_6:9 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "B")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Set (Var "B"))  ($#k10_group_2 :::"/\"::: )  (Set (Var "N"))) "is"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_6 :::"Subgroup"::: )   "of" (Set (Var "B"))) & (Bool (Set (Set (Var "N"))  ($#k10_group_2 :::"/\"::: )  (Set (Var "B"))) "is"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_6 :::"Subgroup"::: )   "of" (Set (Var "B")))  ")" )))) ; 
 definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "B" be    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); let "N" be   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); :: original: :::"/\"::: redefine func "B" :::"/\"::: "N" ->   ($#v15_algstr_0 :::"strict"::: )     ($#v1_group_3 :::"normal"::: )     ($#m1_group_6 :::"Subgroup"::: )   "of" "B"; end; definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "N" be   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); let "B" be    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); :: original: :::"/\"::: redefine func "N" :::"/\"::: "B" ->   ($#v15_algstr_0 :::"strict"::: )     ($#v1_group_3 :::"normal"::: )     ($#m1_group_6 :::"Subgroup"::: )   "of" "B"; end; definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )  ; redefine attr "G" is  :::"trivial":::  means :: GROUP_6:def 2 (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G")  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))); end; 




:: deftheorem    defines :::"trivial"::: GROUP_6:def 2 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )   "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v7_struct_0 :::"trivial"::: )  ) "iff" (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))  ")" )); 
 
theorem :: GROUP_6:10 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k6_group_2 :::"(1)."::: )  (Set (Var "G"))) "is"   ($#v7_struct_0 :::"trivial"::: )  )) ; 
 registrationlet "G" be   ($#l3_algstr_0 :::"Group":::); 
cluster (Set   ($#k6_group_2 :::"(1)."::: )  "G") ->   ($#v7_struct_0 :::"trivial"::: )   ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_struct_0 :::"trivial"::: )     ($#v15_algstr_0 :::"strict"::: )     ($#v1_group_1 :::"unital"::: )     ($#v2_group_1 :::"Group-like"::: )     ($#v3_group_1 :::"associative"::: )    for    ($#l3_algstr_0 :::"multMagma"::: )  ; 
end; 
theorem :: GROUP_6:11 (Bool  "("  (Bool  "("   "for" (Set (Var "G")) "being"   ($#v7_struct_0 :::"trivial"::: )    ($#l3_algstr_0 :::"Group":::) "holds"   (Bool  "("  (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "G")) "is"   ($#v8_struct_0 :::"finite"::: )  )  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Var "G")) "is"   ($#v7_struct_0 :::"trivial"::: )  )  ")" )  ")" ) ; 
 
theorem :: GROUP_6:12 (Bool  "for" (Set (Var "G")) "being"   ($#v7_struct_0 :::"trivial"::: )     ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k6_group_2 :::"(1)."::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Var "G")))) ; 
 notationlet "G" be   ($#l3_algstr_0 :::"Group":::); let "N" be   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); synonym  :::"Cosets"::: "N" for  :::"Left_Cosets"::: "N"; end; registrationlet "G" be   ($#l3_algstr_0 :::"Group":::); let "N" be   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); 
cluster (Set   ($#k15_group_2 :::"Cosets"::: )  "N") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: GROUP_6:13 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k15_group_2 :::"Cosets"::: )  (Set (Var "N"))))) "holds"  (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k13_group_2 :::"*"::: )  (Set (Var "N")))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "N"))  ($#k14_group_2 :::"*"::: )  (Set (Var "a"))))  ")" ))))) ; 
 
theorem :: GROUP_6:14 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k13_group_2 :::"*"::: )  (Set (Var "N")))  ($#r2_hidden :::"in"::: )  (Set   ($#k15_group_2 :::"Cosets"::: )  (Set (Var "N")))) & (Bool (Set (Set (Var "N"))  ($#k14_group_2 :::"*"::: )  (Set (Var "a")))  ($#r2_hidden :::"in"::: )  (Set   ($#k15_group_2 :::"Cosets"::: )  (Set (Var "N"))))  ")" )))) ; 
 
theorem :: GROUP_6:15 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k15_group_2 :::"Cosets"::: )  (Set (Var "N"))))) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")))))) ; 
 
theorem :: GROUP_6:16 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "A1")) "," (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "A1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k15_group_2 :::"Cosets"::: )  (Set (Var "N")))) & (Bool (Set (Var "A2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k15_group_2 :::"Cosets"::: )  (Set (Var "N"))))) "holds"  (Bool (Set (Set (Var "A1"))  ($#k2_group_2 :::"*"::: )  (Set (Var "A2")))  ($#r2_hidden :::"in"::: )  (Set   ($#k15_group_2 :::"Cosets"::: )  (Set (Var "N"))))))) ; 
 definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "N" be   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); func  :::"CosOp"::: "N" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k15_group_2 :::"Cosets"::: )  "N" ")" ) means :: GROUP_6:def 3 (Bool  "for" (Set (Var "W1")) "," (Set (Var "W2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k15_group_2 :::"Cosets"::: )  "N")  (Bool  "for" (Set (Var "A1")) "," (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "G"  "st" (Bool (Bool (Set (Var "W1"))  ($#r1_hidden :::"="::: )  (Set (Var "A1"))) & (Bool (Set (Var "W2"))  ($#r1_hidden :::"="::: )  (Set (Var "A2")))) "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A1"))  ($#k2_group_2 :::"*"::: )  (Set (Var "A2")))))); end; 






:: deftheorem    defines :::"CosOp"::: GROUP_6:def 3 :  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k15_group_2 :::"Cosets"::: )  (Set (Var "N")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_group_6 :::"CosOp"::: )  (Set (Var "N")))) "iff" (Bool  "for" (Set (Var "W1")) "," (Set (Var "W2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k15_group_2 :::"Cosets"::: )  (Set (Var "N")))  (Bool  "for" (Set (Var "A1")) "," (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "W1"))  ($#r1_hidden :::"="::: )  (Set (Var "A1"))) & (Bool (Set (Var "W2"))  ($#r1_hidden :::"="::: )  (Set (Var "A2")))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A1"))  ($#k2_group_2 :::"*"::: )  (Set (Var "A2"))))))  ")" )))); 
 definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "N" be   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); func "G" :::"./."::: "N" ->    ($#l3_algstr_0 :::"multMagma"::: )   equals :: GROUP_6:def 4 (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "("  ($#k15_group_2 :::"Cosets"::: )  "N" ")" ) "," (Set  "("  ($#k4_group_6 :::"CosOp"::: )  "N" ")" ) "#)" ); end; 






:: deftheorem    defines :::"./."::: GROUP_6:def 4 :  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "("  ($#k15_group_2 :::"Cosets"::: )  (Set (Var "N")) ")" ) "," (Set  "("  ($#k4_group_6 :::"CosOp"::: )  (Set (Var "N")) ")" ) "#)" )))); 
 registrationlet "G" be   ($#l3_algstr_0 :::"Group":::); let "N" be   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); 
cluster (Set "G"  ($#k5_group_6 :::"./."::: )  "N") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v15_algstr_0 :::"strict"::: )   ; 
end; 
theorem :: GROUP_6:17 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k15_group_2 :::"Cosets"::: )  (Set (Var "N")))))) ; 
 
theorem :: GROUP_6:18 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")) ")" ))  ($#r1_funct_2 :::"="::: )  (Set   ($#k4_group_6 :::"CosOp"::: )  (Set (Var "N")))))) ; 
 







definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "N" be   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); let "S" be   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Const "G"))  ($#k5_group_6 :::"./."::: )  (Set (Const "N")) ")" ); func  :::"@"::: "S" ->   ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_6:def 5 "S"; end; 







:: deftheorem    defines :::"@"::: GROUP_6:def 5 :  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")) ")" ) "holds"  (Bool (Set   ($#k6_group_6 :::"@"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set (Var "S")))))); 
 
theorem :: GROUP_6:19 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")) ")" ) "holds"  (Bool (Set (Set  "("  ($#k6_group_6 :::"@"::: )  (Set (Var "T1")) ")" )  ($#k2_group_2 :::"*"::: )  (Set  "("  ($#k6_group_6 :::"@"::: )  (Set (Var "T2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "T1"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "T2"))))))) ; 
 
theorem :: GROUP_6:20 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")) ")" ) "holds"  (Bool (Set   ($#k6_group_6 :::"@"::: )  (Set  "(" (Set (Var "T1"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "T2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_group_6 :::"@"::: )  (Set (Var "T1")) ")" )  ($#k2_group_2 :::"*"::: )  (Set  "("  ($#k6_group_6 :::"@"::: )  (Set (Var "T2")) ")" )))))) ; 
 registrationlet "G" be   ($#l3_algstr_0 :::"Group":::); let "N" be   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); 
cluster (Set "G"  ($#k5_group_6 :::"./."::: )  "N") ->   ($#v2_group_1 :::"Group-like"::: )     ($#v3_group_1 :::"associative"::: )   ; 
end; 
theorem :: GROUP_6:21 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")) ")" ) (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "S"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k13_group_2 :::"*"::: )  (Set (Var "N")))) & (Bool (Set (Var "S"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "N"))  ($#k14_group_2 :::"*"::: )  (Set (Var "a"))))  ")" ))))) ; 
 
theorem :: GROUP_6:22 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Set (Var "N"))  ($#k14_group_2 :::"*"::: )  (Set (Var "a"))) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")) ")" )) & (Bool (Set (Set (Var "a"))  ($#k13_group_2 :::"*"::: )  (Set (Var "N"))) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")) ")" )) & (Bool (Set   ($#k8_group_2 :::"carr"::: )  (Set (Var "N"))) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")) ")" ))  ")" )))) ; 
 
theorem :: GROUP_6:23 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_struct_0 :::"in"::: )  (Set (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")))) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k13_group_2 :::"*"::: )  (Set (Var "N")))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "N"))  ($#k14_group_2 :::"*"::: )  (Set (Var "a"))))  ")" ))  ")" )))) ; 
 
theorem :: GROUP_6:24 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k1_group_1 :::"1_"::: )  (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k8_group_2 :::"carr"::: )  (Set (Var "N")))))) ; 
 
theorem :: GROUP_6:25 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")) ")" )  "st" (Bool (Bool (Set (Var "S"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k13_group_2 :::"*"::: )  (Set (Var "N"))))) "holds"  (Bool (Set (Set (Var "S"))  ($#k2_group_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_group_1 :::"""::: )  ")" )  ($#k13_group_2 :::"*"::: )  (Set (Var "N")))))))) ; 
 
theorem :: GROUP_6:26 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k7_struct_0 :::"card"::: )  (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k17_group_2 :::"Index"::: )  (Set (Var "N")))))) ; 
 
theorem :: GROUP_6:27 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set   ($#k15_group_2 :::"Left_Cosets"::: )  (Set (Var "N"))) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool (Set   ($#k7_struct_0 :::"card"::: )  (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k18_group_2 :::"index"::: )  (Set (Var "N")))))) ; 
 
theorem :: GROUP_6:28 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "B")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "M")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "M")) "is"    ($#m1_group_6 :::"Subgroup"::: )   "of" (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "B"))  ($#k5_group_6 :::"./."::: )  (Set  "("  "(" (Set (Var "B")) "," (Set (Var "M")) ")"   ($#k1_group_6 :::"`*`"::: )  ")" )) "is"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "M"))))))) ; 
 
theorem :: GROUP_6:29 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "," (Set (Var "M")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "M")) "is"    ($#m1_group_6 :::"Subgroup"::: )   "of" (Set (Var "N")))) "holds"  (Bool (Set (Set (Var "N"))  ($#k5_group_6 :::"./."::: )  (Set  "("  "(" (Set (Var "N")) "," (Set (Var "M")) ")"   ($#k1_group_6 :::"`*`"::: )  ")" )) "is"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "M")))))) ; 
 
theorem :: GROUP_6:30 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N"))) "is"   ($#v5_group_1 :::"commutative"::: )    ($#l3_algstr_0 :::"Group":::)) "iff" (Bool (Set (Set (Var "G"))  ($#k9_group_5 :::"`"::: )  ) "is"    ($#m1_group_6 :::"Subgroup"::: )   "of" (Set (Var "N")))  ")" ))) ; 
 definitionlet "G", "H" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_algstr_0 :::"multMagma"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "G")) "," (Set (Const "H")); attr "f" is  :::"multiplicative":::  means :: GROUP_6:def 6 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" "G" "holds"  (Bool (Set "f"  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" )))); end; 






:: deftheorem    defines :::"multiplicative"::: GROUP_6:def 6 :  (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_algstr_0 :::"multMagma"::: )    (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_group_6 :::"multiplicative"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" ))))  ")" ))); 
 registrationlet "G", "H" be   ($#l3_algstr_0 :::"Group":::); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G")  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "H")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  bbbadV1_PARTFUN1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G"))   ($#v1_funct_2 :::"quasi_total"::: )     ($#v1_group_6 :::"multiplicative"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "H") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; definitionlet "G", "H" be   ($#l3_algstr_0 :::"Group":::); mode Homomorphism of "G" "," "H" is   ($#v1_group_6 :::"multiplicative"::: )    ($#m1_subset_1 :::"Function":::) "of" "G" "," "H"; end; 







theorem :: GROUP_6:31 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "H")))))) ; 
 registrationlet "G", "H" be   ($#l3_algstr_0 :::"Group":::); 
cluster   ($#v1_funct_1 :::"Function-like"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v1_group_6 :::"multiplicative"::: )    ->   ($#v6_group_1 :::"unity-preserving"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "H") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; 
theorem :: GROUP_6:32 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "a"))  ($#k2_group_1 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" )  ($#k2_group_1 :::"""::: )  ))))) ; 
 
theorem :: GROUP_6:33 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "a"))  ($#k2_group_3 :::"|^"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" )  ($#k2_group_3 :::"|^"::: )  (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" )))))) ; 
 
theorem :: GROUP_6:34 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_group_5 :::"[."::: ) (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" ) ($#k2_group_5 :::".]"::: ) ))))) ; 
 
theorem :: GROUP_6:35 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k3_group_5 :::"[."::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_group_5 :::".]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k3_group_5 :::"[."::: ) (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a1")) ")" ) "," (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a2")) ")" ) "," (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a3")) ")" ) ($#k3_group_5 :::".]"::: ) ))))) ; 
 
theorem :: GROUP_6:36 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" )  ($#k5_group_1 :::"|^"::: )  (Set (Var "n")))))))) ; 
 
theorem :: GROUP_6:37 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" )  ($#k5_group_1 :::"|^"::: )  (Set (Var "i")))))))) ; 
 
theorem :: GROUP_6:38 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))) "is"   ($#v1_group_6 :::"multiplicative"::: )  )) ; 
 
theorem :: GROUP_6:39 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "I")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H"))  (Bool  "for" (Set (Var "h1")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "H")) "," (Set (Var "I")) "holds"  (Bool (Set (Set (Var "h1"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "h"))) "is"   ($#v1_group_6 :::"multiplicative"::: )  )))) ; 
 registrationlet "G", "H", "I" be   ($#l3_algstr_0 :::"Group":::); let "h" be   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G")) "," (Set (Const "H")); let "h1" be   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "H")) "," (Set (Const "I")); 
cluster (Set "h"  ($#k3_relat_1 :::"*"::: )  "h1") ->   ($#v1_group_6 :::"multiplicative"::: )    for  ($#m1_subset_1 :::"Function":::) "of" "G" "," "I"; 
end; definitionlet "G", "H" be   ($#l3_algstr_0 :::"Group":::); func  :::"1:":::  "(" "G" "," "H" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" "G" "," "H" means :: GROUP_6:def 7 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" "G" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  "H"))); end; 






:: deftheorem    defines :::"1:"::: GROUP_6:def 7 :  (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_group_6 :::"1:"::: )   "(" (Set (Var "G")) "," (Set (Var "H")) ")" )) "iff" (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "H")))))  ")" ))); 
 registrationlet "G", "H" be   ($#l3_algstr_0 :::"Group":::); 
cluster (Set   ($#k7_group_6 :::"1:"::: )   "(" "G" "," "H" ")" ) ->   ($#v1_group_6 :::"multiplicative"::: )   ; 
end; 
theorem :: GROUP_6:40 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "I")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H"))  (Bool  "for" (Set (Var "h1")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "H")) "," (Set (Var "I")) "holds"   (Bool  "("  (Bool (Set (Set (Var "h1"))  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k7_group_6 :::"1:"::: )   "(" (Set (Var "G")) "," (Set (Var "H")) ")"  ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k7_group_6 :::"1:"::: )   "(" (Set (Var "G")) "," (Set (Var "I")) ")" )) & (Bool (Set (Set  "("  ($#k7_group_6 :::"1:"::: )   "(" (Set (Var "H")) "," (Set (Var "I")) ")"  ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "h")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k7_group_6 :::"1:"::: )   "(" (Set (Var "G")) "," (Set (Var "I")) ")" ))  ")" )))) ; 
 definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "N" be   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); func  :::"nat_hom"::: "N" ->   ($#m1_subset_1 :::"Function":::) "of" "G" "," (Set  "(" "G"  ($#k5_group_6 :::"./."::: )  "N" ")" ) means :: GROUP_6:def 8 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" "G" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k13_group_2 :::"*"::: )  "N"))); end; 






:: deftheorem    defines :::"nat_hom"::: GROUP_6:def 8 :  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_group_6 :::"nat_hom"::: )  (Set (Var "N")))) "iff" (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k13_group_2 :::"*"::: )  (Set (Var "N")))))  ")" )))); 
 registrationlet "G" be   ($#l3_algstr_0 :::"Group":::); let "N" be   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); 
cluster (Set   ($#k8_group_6 :::"nat_hom"::: )  "N") ->   ($#v1_group_6 :::"multiplicative"::: )   ; 
end; definitionlet "G", "H" be   ($#l3_algstr_0 :::"Group":::); let "g" be   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G")) "," (Set (Const "H")); func  :::"Ker"::: "g" ->   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" "G" means :: GROUP_6:def 9 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )   "{"  (Set (Var "a")) where a "is"   ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool (Set "g"  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  "H"))  "}"  ); end; 







:: deftheorem    defines :::"Ker"::: GROUP_6:def 9 :  (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H"))  (Bool  "for" (Set (Var "b4")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_group_6 :::"Ker"::: )  (Set (Var "g")))) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "a")) where a "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "H"))))  "}"  )  ")" )))); 
 registrationlet "G", "H" be   ($#l3_algstr_0 :::"Group":::); let "g" be   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G")) "," (Set (Const "H")); 
cluster (Set   ($#k9_group_6 :::"Ker"::: )  "g") ->   ($#v15_algstr_0 :::"strict"::: )     ($#v1_group_3 :::"normal"::: )   ; 
end; 
theorem :: GROUP_6:41 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k9_group_6 :::"Ker"::: )  (Set (Var "h")))) "iff" (Bool (Set (Set (Var "h"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "H"))))  ")" )))) ; 
 
theorem :: GROUP_6:42 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k9_group_6 :::"Ker"::: )  (Set  "("  ($#k7_group_6 :::"1:"::: )   "(" (Set (Var "G")) "," (Set (Var "H")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "G")))) ; 
 
theorem :: GROUP_6:43 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k9_group_6 :::"Ker"::: )  (Set  "("  ($#k8_group_6 :::"nat_hom"::: )  (Set (Var "N")) ")" ))  ($#r1_group_2 :::"="::: )  (Set (Var "N"))))) ; 
 definitionlet "G", "H" be   ($#l3_algstr_0 :::"Group":::); let "g" be   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G")) "," (Set (Const "H")); func  :::"Image"::: "g" ->   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" "H" means :: GROUP_6:def 10 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set "g"  ($#k7_relset_1 :::".:"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G"))); end; 







:: deftheorem    defines :::"Image"::: GROUP_6:def 10 :  (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H"))  (Bool  "for" (Set (Var "b4")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "H")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_group_6 :::"Image"::: )  (Set (Var "g")))) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k7_relset_1 :::".:"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))))  ")" )))); 
 
theorem :: GROUP_6:44 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k10_group_6 :::"Image"::: )  (Set (Var "g")) ")" ))))) ; 
 
theorem :: GROUP_6:45 (Bool  "for" (Set (Var "H")) "," (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k10_group_6 :::"Image"::: )  (Set (Var "g")))) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))))  ")" )))) ; 
 
theorem :: GROUP_6:46 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"  (Bool (Set   ($#k10_group_6 :::"Image"::: )  (Set (Var "g")))  ($#r1_group_2 :::"="::: )  (Set   ($#k5_group_4 :::"gr"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")) ")" ))))) ; 
 
theorem :: GROUP_6:47 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k10_group_6 :::"Image"::: )  (Set  "("  ($#k7_group_6 :::"1:"::: )   "(" (Set (Var "G")) "," (Set (Var "H")) ")"  ")" ))  ($#r1_group_2 :::"="::: )  (Set   ($#k6_group_2 :::"(1)."::: )  (Set (Var "H"))))) ; 
 
theorem :: GROUP_6:48 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k10_group_6 :::"Image"::: )  (Set  "("  ($#k8_group_6 :::"nat_hom"::: )  (Set (Var "N")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")))))) ; 
 
theorem :: GROUP_6:49 (Bool  "for" (Set (Var "H")) "," (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"  (Bool (Set (Var "h")) "is"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set  "("  ($#k10_group_6 :::"Image"::: )  (Set (Var "h")) ")" )))) ; 
 
theorem :: GROUP_6:50 (Bool  "for" (Set (Var "H")) "," (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H"))  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v8_struct_0 :::"finite"::: )  )) "holds"  (Bool (Set   ($#k10_group_6 :::"Image"::: )  (Set (Var "g"))) "is"   ($#v8_struct_0 :::"finite"::: )  ))) ; 
 registrationlet "G" be   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::); let "H" be   ($#l3_algstr_0 :::"Group":::); let "g" be   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G")) "," (Set (Const "H")); 
cluster (Set   ($#k10_group_6 :::"Image"::: )  "g") ->   ($#v8_struct_0 :::"finite"::: )     ($#v15_algstr_0 :::"strict"::: )   ; 
end; 
theorem :: GROUP_6:51 (Bool  "for" (Set (Var "H")) "," (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H"))  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v5_group_1 :::"commutative"::: )    ($#l3_algstr_0 :::"Group":::))) "holds"  (Bool (Set   ($#k10_group_6 :::"Image"::: )  (Set (Var "g"))) "is"   ($#v5_group_1 :::"commutative"::: )  ))) ; 
 
theorem :: GROUP_6:52 (Bool  "for" (Set (Var "H")) "," (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"  (Bool (Set   ($#k7_struct_0 :::"card"::: )  (Set  "("  ($#k10_group_6 :::"Image"::: )  (Set (Var "g")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k7_struct_0 :::"card"::: )  (Set (Var "G")))))) ; 
 
theorem :: GROUP_6:53 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"  (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set  "("  ($#k10_group_6 :::"Image"::: )  (Set (Var "g")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "G"))))))) ; 
 
theorem :: GROUP_6:54 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H"))  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H"))  "st" (Bool (Bool (Set (Var "h")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "c"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k10_group_6 :::"Image"::: )  (Set (Var "h"))))) "holds"  (Bool (Set (Set (Var "h"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "h"))  ($#k2_funct_1 :::"""::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "c")))))) ; 
 
theorem :: GROUP_6:55 (Bool  "for" (Set (Var "H")) "," (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H"))  "st" (Bool (Bool (Set (Var "h")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool (Set (Set (Var "h"))  ($#k2_funct_1 :::"""::: )  ) "is"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set  "("  ($#k10_group_6 :::"Image"::: )  (Set (Var "h")) ")" ) "," (Set (Var "G"))))) ; 
 
theorem :: GROUP_6:56 (Bool  "for" (Set (Var "H")) "," (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"   (Bool  "("  (Bool (Set (Var "h")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) "iff" (Bool (Set   ($#k9_group_6 :::"Ker"::: )  (Set (Var "h")))  ($#r1_group_2 :::"="::: )  (Set   ($#k6_group_2 :::"(1)."::: )  (Set (Var "G"))))  ")" ))) ; 
 
theorem :: GROUP_6:57 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "H")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"   (Bool  "("  (Bool (Set (Var "h")) "is"   ($#v2_funct_2 :::"onto"::: )  ) "iff" (Bool (Set   ($#k10_group_6 :::"Image"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set (Var "H")))  ")" )))) ; 
 
theorem :: GROUP_6:58 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H"))  "st" (Bool (Bool (Set (Var "h")) "is"   ($#v2_funct_2 :::"onto"::: )  )) "holds"  (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "H")) (Bool  "ex" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "G")) "st" (Bool (Set (Set (Var "h"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "c"))))))) ; 
 
theorem :: GROUP_6:59 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k8_group_6 :::"nat_hom"::: )  (Set (Var "N"))) "is"   ($#v2_funct_2 :::"onto"::: )  ))) ; 
 
theorem :: GROUP_6:60 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"   (Bool  "("  (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  ) "iff" (Bool  "("  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set (Var "H"))) & (Bool (Set (Var "h")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )  ")" )  ")" ))) ; 
 
theorem :: GROUP_6:61 (Bool  "for" (Set (Var "G")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "H")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H"))  "st" (Bool (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set (Var "G"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set (Var "H")))  ")" )))) ; 
 
theorem :: GROUP_6:62 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "H")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H"))  "st" (Bool (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  )) "holds"  (Bool (Set (Set (Var "h"))  ($#k2_funct_1 :::"""::: )  ) "is"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "H")) "," (Set (Var "G")))))) ; 
 
theorem :: GROUP_6:63 (Bool  "for" (Set (Var "G")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "H")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H"))  (Bool  "for" (Set (Var "g1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "H")) "," (Set (Var "G"))  "st" (Bool (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  ) & (Bool (Set (Var "g1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "h"))  ($#k2_funct_1 :::"""::: )  ))) "holds"  (Bool (Set (Var "g1")) "is"   ($#v3_funct_2 :::"bijective"::: )  ))))) ; 
 
theorem :: GROUP_6:64 (Bool  "for" (Set (Var "G")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "H")) "," (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H"))  (Bool  "for" (Set (Var "h1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "H")) "," (Set (Var "I"))  "st" (Bool (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  ) & (Bool (Set (Var "h1")) "is"   ($#v3_funct_2 :::"bijective"::: )  )) "holds"  (Bool (Set (Set (Var "h1"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "h"))) "is"   ($#v3_funct_2 :::"bijective"::: )  ))))) ; 
 
theorem :: GROUP_6:65 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k8_group_6 :::"nat_hom"::: )  (Set  "("  ($#k6_group_2 :::"(1)."::: )  (Set (Var "G")) ")" )) "is"   ($#v3_funct_2 :::"bijective"::: )  )) ; 
 definitionlet "G", "H" be   ($#l3_algstr_0 :::"Group":::); pred "G" "," "H" :::"are_isomorphic":::  means :: GROUP_6:def 11 (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" "G" "," "H" "st" (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  )); reflexivity  
(Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::) (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "G")) "st" (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  )))
 ; end; 





:: deftheorem    defines :::"are_isomorphic"::: GROUP_6:def 11 :  (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::) "holds"   (Bool  "("  (Bool (Set (Var "G")) "," (Set (Var "H"))  ($#r1_group_6 :::"are_isomorphic"::: )  ) "iff" (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  ))  ")" )); 
 
theorem :: GROUP_6:66 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set (Var "G")) "," (Set (Var "H"))  ($#r1_group_6 :::"are_isomorphic"::: )  )) "holds"  (Bool (Set (Var "H")) "," (Set (Var "G"))  ($#r1_group_6 :::"are_isomorphic"::: )  )) ; 
 definitionlet "G", "H" be   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::); :: original: :::"are_isomorphic"::: redefine pred "G" "," "H" :::"are_isomorphic"::: ; symmetry  
(Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool ((Set (Var "b1")) "," (Set (Var "b2"))))) "holds"  (Bool ((Set (Var "b2")) "," (Set (Var "b1")))))
 ; end; 
theorem :: GROUP_6:67 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "I")) "being"   ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set (Var "G")) "," (Set (Var "H"))  ($#r1_group_6 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "H")) "," (Set (Var "I"))  ($#r1_group_6 :::"are_isomorphic"::: )  )) "holds"  (Bool (Set (Var "G")) "," (Set (Var "I"))  ($#r1_group_6 :::"are_isomorphic"::: )  )) ; 
 
theorem :: GROUP_6:68 (Bool  "for" (Set (Var "H")) "," (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H"))  "st" (Bool (Bool (Set (Var "h")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool (Set (Var "G")) "," (Set   ($#k10_group_6 :::"Image"::: )  (Set (Var "h")))  ($#r1_group_6 :::"are_isomorphic"::: )  ))) ; 
 
theorem :: GROUP_6:69 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v7_struct_0 :::"trivial"::: )  ) & (Bool (Set (Var "H")) "is"   ($#v7_struct_0 :::"trivial"::: )  )) "holds"  (Bool (Set (Var "G")) "," (Set (Var "H"))  ($#r2_group_6 :::"are_isomorphic"::: )  )) ; 
 
theorem :: GROUP_6:70 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k6_group_2 :::"(1)."::: )  (Set (Var "G"))) "," (Set   ($#k6_group_2 :::"(1)."::: )  (Set (Var "H")))  ($#r2_group_6 :::"are_isomorphic"::: )  )) ; 
 
theorem :: GROUP_6:71 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set (Var "G")) "," (Set (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set  "("  ($#k6_group_2 :::"(1)."::: )  (Set (Var "G")) ")" ))  ($#r2_group_6 :::"are_isomorphic"::: )  )) ; 
 
theorem :: GROUP_6:72 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set  "("  ($#k7_group_2 :::"(Omega)."::: )  (Set (Var "G")) ")" )) "is"   ($#v7_struct_0 :::"trivial"::: )  )) ; 
 
theorem :: GROUP_6:73 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set (Var "G")) "," (Set (Var "H"))  ($#r2_group_6 :::"are_isomorphic"::: )  )) "holds"  (Bool (Set   ($#k7_struct_0 :::"card"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_struct_0 :::"card"::: )  (Set (Var "H"))))) ; 
 
theorem :: GROUP_6:74 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set (Var "G")) "," (Set (Var "H"))  ($#r1_group_6 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v8_struct_0 :::"finite"::: )  )) "holds"  (Bool (Set (Var "H")) "is"   ($#v8_struct_0 :::"finite"::: )  )) ; 
 
theorem :: GROUP_6:75 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set (Var "G")) "," (Set (Var "H"))  ($#r2_group_6 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v8_struct_0 :::"finite"::: )  )) "holds"  (Bool (Set   ($#k7_struct_0 :::"card"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_struct_0 :::"card"::: )  (Set (Var "H"))))) ; 
 
theorem :: GROUP_6:76 (Bool  "for" (Set (Var "G")) "being"   ($#v7_struct_0 :::"trivial"::: )     ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "H")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set (Var "G")) "," (Set (Var "H"))  ($#r2_group_6 :::"are_isomorphic"::: )  )) "holds"  (Bool (Set (Var "H")) "is"   ($#v7_struct_0 :::"trivial"::: )  ))) ; 
 
theorem :: GROUP_6:77 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "H")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set (Var "G")) "," (Set (Var "H"))  ($#r1_group_6 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v5_group_1 :::"commutative"::: )  )) "holds"  (Bool (Set (Var "H")) "is"   ($#v5_group_1 :::"commutative"::: )  ))) ; 
 
theorem :: GROUP_6:78 (Bool  "for" (Set (Var "H")) "," (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"  (Bool (Set (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set  "("  ($#k9_group_6 :::"Ker"::: )  (Set (Var "g")) ")" )) "," (Set   ($#k10_group_6 :::"Image"::: )  (Set (Var "g")))  ($#r2_group_6 :::"are_isomorphic"::: )  ))) ; 
 
theorem :: GROUP_6:79 (Bool  "for" (Set (Var "H")) "," (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set  "("  ($#k9_group_6 :::"Ker"::: )  (Set (Var "g")) ")" ) ")" ) "," (Set  "("  ($#k10_group_6 :::"Image"::: )  (Set (Var "g")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  ) & (Bool (Set (Var "g"))  ($#r1_funct_2 :::"="::: )  (Set (Set (Var "h"))  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k8_group_6 :::"nat_hom"::: )  (Set  "("  ($#k9_group_6 :::"Ker"::: )  (Set (Var "g")) ")" ) ")" )))  ")" )))) ; 
 
theorem :: GROUP_6:80 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "N")) "being"   ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "M")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "J")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "M")))  "st" (Bool (Bool (Set (Var "J"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "N"))  ($#k5_group_6 :::"./."::: )  (Set  "("  "(" (Set (Var "N")) "," (Set (Var "M")) ")"   ($#k1_group_6 :::"`*`"::: )  ")" ))) & (Bool (Set (Var "M")) "is"    ($#m1_group_6 :::"Subgroup"::: )   "of" (Set (Var "N")))) "holds"  (Bool (Set (Set  "(" (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "M")) ")" )  ($#k5_group_6 :::"./."::: )  (Set (Var "J"))) "," (Set (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set (Var "N")))  ($#r2_group_6 :::"are_isomorphic"::: )  ))))) ; 
 
theorem :: GROUP_6:81 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "B")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "N")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set (Set  "(" (Set (Var "B"))  ($#k8_group_4 :::""\/""::: )  (Set (Var "N")) ")" )  ($#k5_group_6 :::"./."::: )  (Set  "("  "(" (Set  "(" (Set (Var "B"))  ($#k8_group_4 :::""\/""::: )  (Set (Var "N")) ")" ) "," (Set (Var "N")) ")"   ($#k1_group_6 :::"`*`"::: )  ")" )) "," (Set (Set (Var "B"))  ($#k5_group_6 :::"./."::: )  (Set  "(" (Set (Var "B"))  ($#k2_group_6 :::"/\"::: )  (Set (Var "N")) ")" ))  ($#r2_group_6 :::"are_isomorphic"::: )  )))) ;