:: GROUP_5 semantic presentation begin theorem :: GROUP_5:1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) ")" ))) ; theorem :: GROUP_5:2 (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")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) & (Bool (Set (Var "b")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))) "holds" (Bool (Set (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))))) ; theorem :: GROUP_5:3 (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")) (Bool "for" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "N")))))) ; theorem :: GROUP_5:4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2")))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))) & (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1"))) & (Bool (Set (Var "b")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H2"))) ")" )) ")" )))) ; theorem :: GROUP_5:5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H2")) ($#k7_group_4 :::"*"::: ) (Set (Var "H1"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2")))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))) & (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1"))) & (Bool (Set (Var "b")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H2"))) ")" )) ")" )))) ; theorem :: GROUP_5:6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2")))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))) & (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1"))) & (Bool (Set (Var "b")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H2"))) ")" )) ")" )))) ; theorem :: GROUP_5:7 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#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 "N1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "N2")))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))) & (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "N1"))) & (Bool (Set (Var "b")) ($#r1_struct_0 :::"in"::: ) (Set (Var "N2"))) ")" )) ")" )))) ; theorem :: GROUP_5:8 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "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 (Set (Set (Var "H")) ($#k7_group_4 :::"*"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k7_group_4 :::"*"::: ) (Set (Var "H"))))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G"))); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func "F" :::"|^"::: "a" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") means :: GROUP_5:def 1 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "F")) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "F"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k2_group_3 :::"|^"::: ) "a")) ")" ) ")" ); end; :: deftheorem defines :::"|^"::: GROUP_5:def 1 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_group_5 :::"|^"::: ) (Set (Var "a")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k2_group_3 :::"|^"::: ) (Set (Var "a")))) ")" ) ")" ) ")" ))))); theorem :: GROUP_5:9 (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 "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool (Set (Set "(" (Set (Var "F1")) ($#k1_group_5 :::"|^"::: ) (Set (Var "a")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "F2")) ($#k1_group_5 :::"|^"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "F2")) ")" ) ($#k1_group_5 :::"|^"::: ) (Set (Var "a"))))))) ; theorem :: GROUP_5:10 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" ) ($#k1_group_5 :::"|^"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: GROUP_5:11 (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 (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k1_group_5 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )))) ; theorem :: GROUP_5:12 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_finseq_4 :::"*>"::: ) ) ($#k1_group_5 :::"|^"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "b")) ($#k2_group_3 :::"|^"::: ) (Set (Var "c")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )))) ; theorem :: GROUP_5:13 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k3_finseq_4 :::"*>"::: ) ) ($#k1_group_5 :::"|^"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "d")) ")" ) "," (Set "(" (Set (Var "b")) ($#k2_group_3 :::"|^"::: ) (Set (Var "d")) ")" ) "," (Set "(" (Set (Var "c")) ($#k2_group_3 :::"|^"::: ) (Set (Var "d")) ")" ) ($#k3_finseq_4 :::"*>"::: ) )))) ; theorem :: GROUP_5: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 "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "F")) ($#k1_group_5 :::"|^"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "F")) ")" ) ($#k2_group_3 :::"|^"::: ) (Set (Var "a"))))))) ; theorem :: GROUP_5:15 (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 "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "I")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_group_5 :::"|^"::: ) (Set (Var "a")) ")" ) ($#k4_group_4 :::"|^"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_group_4 :::"|^"::: ) (Set (Var "I")) ")" ) ($#k1_group_5 :::"|^"::: ) (Set (Var "a")))))))) ; begin definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func :::"[.":::"a" "," "b":::".]"::: -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: GROUP_5:def 2 (Set (Set "(" (Set "(" (Set "(" "a" ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" "b" ($#k2_group_1 :::"""::: ) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) "a" ")" ) ($#k6_algstr_0 :::"*"::: ) "b"); end; :: deftheorem defines :::"[."::: GROUP_5:def 2 : (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 (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))))); theorem :: GROUP_5:16 (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 ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))) & (Bool (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))) & (Bool (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ))) & (Bool (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ))) & (Bool (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ))) ")" ))) ; theorem :: GROUP_5:17 (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 (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ))))) ; theorem :: GROUP_5:18 (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 ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k2_group_3 :::"|^"::: ) (Set (Var "a")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))) & (Bool (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ))) ")" ))) ; theorem :: GROUP_5:19 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k2_group_5 :::"[."::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) "," (Set (Var "a")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) & (Bool (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) ")" ))) ; theorem :: GROUP_5:20 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "a")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; theorem :: GROUP_5:21 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) & (Bool (Set ($#k2_group_5 :::"[."::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set (Var "a")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) ")" ))) ; theorem :: GROUP_5:22 (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 (Set (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_group_5 :::"[."::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k2_group_5 :::".]"::: ) )))) ; theorem :: GROUP_5:23 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k2_group_5 :::"[."::: ) (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "b")) ($#k2_group_3 :::"|^"::: ) (Set (Var "c")) ")" ) ($#k2_group_5 :::".]"::: ) )))) ; theorem :: GROUP_5:24 (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 (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k5_group_1 :::"|^"::: ) (Num 2) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ")" ) ($#k5_group_1 :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k5_group_1 :::"|^"::: ) (Num 2) ")" ))))) ; theorem :: GROUP_5:25 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k2_group_5 :::"[."::: ) (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) "," (Set (Var "c")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set ($#k2_group_5 :::"[."::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k2_group_5 :::".]"::: ) ))))) ; theorem :: GROUP_5:26 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c")) ")" ) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k2_group_5 :::".]"::: ) ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set (Var "c")) ")" ))))) ; theorem :: GROUP_5:27 (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 (Set ($#k2_group_5 :::"[."::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_group_5 :::"[."::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ))))) ; theorem :: GROUP_5:28 (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 (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_group_5 :::"[."::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ))))) ; theorem :: GROUP_5:29 (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 ($#k2_group_5 :::"[."::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k2_group_1 :::"""::: ) ")" ))) & (Bool (Set ($#k2_group_5 :::"[."::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k2_group_1 :::"""::: ) ")" ))) ")" ))) ; theorem :: GROUP_5:30 (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 (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k2_group_3 :::"|^"::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ")" ) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_group_5 :::"[."::: ) (Set (Var "b")) "," (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k2_group_5 :::".]"::: ) )))) ; theorem :: GROUP_5:31 (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 (Set ($#k2_group_5 :::"[."::: ) (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ")" ) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_group_5 :::"[."::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set (Var "a")) ($#k2_group_5 :::".]"::: ) )))) ; theorem :: GROUP_5:32 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 (Set ($#k2_group_5 :::"[."::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n")) ")" ) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) ($#k5_group_1 :::"|^"::: ) (Set (Var "n")) ")" )))))) ; theorem :: GROUP_5:33 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n")) ")" ) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "b")) ($#k2_group_3 :::"|^"::: ) (Set (Var "a")) ")" ) ($#k5_group_1 :::"|^"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n")) ")" )))))) ; theorem :: GROUP_5:34 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (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 (Set ($#k2_group_5 :::"[."::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" ) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "i")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" )))))) ; theorem :: GROUP_5:35 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (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 (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" ) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "b")) ($#k2_group_3 :::"|^"::: ) (Set (Var "a")) ")" ) ($#k5_group_1 :::"|^"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "i")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" )))))) ; theorem :: GROUP_5:36 (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 ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) "iff" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")))) ")" ))) ; theorem :: GROUP_5:37 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::)) "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_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))))) ")" )) ; theorem :: GROUP_5:38 (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")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) & (Bool (Set (Var "b")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))) "holds" (Bool (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "a", "b", "c" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func :::"[.":::"a" "," "b" "," "c":::".]"::: -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: GROUP_5:def 3 (Set ($#k2_group_5 :::"[."::: ) (Set ($#k2_group_5 :::"[."::: ) "a" "," "b" ($#k2_group_5 :::".]"::: ) ) "," "c" ($#k2_group_5 :::".]"::: ) ); end; :: deftheorem defines :::"[."::: GROUP_5:def 3 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k3_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_group_5 :::"[."::: ) (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) "," (Set (Var "c")) ($#k2_group_5 :::".]"::: ) )))); theorem :: GROUP_5:39 (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 ($#k3_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k3_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) & (Bool (Set ($#k3_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) "," (Set (Var "b")) ($#k3_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) & (Bool (Set ($#k3_group_5 :::"[."::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) "," (Set (Var "a")) "," (Set (Var "b")) ($#k3_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) ")" ))) ; theorem :: GROUP_5:40 (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 (Set ($#k3_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "b")) ($#k3_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; theorem :: GROUP_5:41 (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 (Set ($#k3_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a")) ($#k3_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_group_5 :::"[."::: ) (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) "," (Set (Var "a")) ($#k2_group_5 :::".]"::: ) )))) ; theorem :: GROUP_5:42 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_group_5 :::"[."::: ) (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "a")) ($#k3_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_group_5 :::"[."::: ) (Set (Var "b")) "," (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k2_group_5 :::".]"::: ) ) ($#k6_algstr_0 :::"*"::: ) (Set ($#k2_group_5 :::"[."::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k2_group_5 :::".]"::: ) ) ")" ) ($#k2_group_3 :::"|^"::: ) (Set (Var "a")))))) ; theorem :: GROUP_5:43 (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 (Set ($#k3_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "b")) ($#k2_group_3 :::"|^"::: ) (Set (Var "a")) ")" ) ($#k3_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_group_5 :::"[."::: ) (Set (Var "b")) "," (Set ($#k2_group_5 :::"[."::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_5 :::".]"::: ) )))) ; theorem :: GROUP_5:44 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k2_group_5 :::"[."::: ) (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) "," (Set (Var "c")) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k2_group_5 :::".]"::: ) ) ($#k6_algstr_0 :::"*"::: ) (Set ($#k3_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) ($#k3_group_5 :::".]"::: ) ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set ($#k2_group_5 :::"[."::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k2_group_5 :::".]"::: ) ))))) ; theorem :: GROUP_5:45 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c")) ")" ) ($#k2_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k2_group_5 :::".]"::: ) ) ($#k6_algstr_0 :::"*"::: ) (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set ($#k3_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k3_group_5 :::".]"::: ) ))))) ; theorem :: GROUP_5:46 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k3_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set (Var "c")) ($#k3_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set ($#k3_group_5 :::"[."::: ) (Set (Var "b")) "," (Set "(" (Set (Var "c")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set (Var "a")) ($#k3_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set (Var "c")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set ($#k3_group_5 :::"[."::: ) (Set (Var "c")) "," (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set (Var "b")) ($#k3_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); func :::"commutators"::: "(" "A" "," "B" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_5:def 4 "{" (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) where a, b "is" ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) "B") ")" ) "}" ; end; :: deftheorem defines :::"commutators"::: GROUP_5:def 4 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k4_group_5 :::"commutators"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#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 "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" ))); theorem :: GROUP_5:47 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_group_5 :::"commutators"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) )) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" )) ")" )))) ; theorem :: GROUP_5:48 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k4_group_5 :::"commutators"::: ) "(" (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" ) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_group_5 :::"commutators"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: GROUP_5:49 (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 (Set ($#k4_group_5 :::"commutators"::: ) "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) "," (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "b")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: GROUP_5:50 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k4_group_5 :::"commutators"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_group_5 :::"commutators"::: ) "(" (Set (Var "B")) "," (Set (Var "D")) ")" )))) ; theorem :: GROUP_5:51 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::)) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k4_group_5 :::"commutators"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ")" )) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H1", "H2" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); func :::"commutators"::: "(" "H1" "," "H2" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_5:def 5 (Set ($#k4_group_5 :::"commutators"::: ) "(" (Set "(" ($#k8_group_2 :::"carr"::: ) "H1" ")" ) "," (Set "(" ($#k8_group_2 :::"carr"::: ) "H2" ")" ) ")" ); end; :: deftheorem defines :::"commutators"::: GROUP_5:def 5 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k5_group_5 :::"commutators"::: ) "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_group_5 :::"commutators"::: ) "(" (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" ) "," (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" ) ")" )))); theorem :: GROUP_5:52 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_group_5 :::"commutators"::: ) "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" )) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) )) & (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1"))) & (Bool (Set (Var "b")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H2"))) ")" )) ")" )))) ; theorem :: GROUP_5:53 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_group_5 :::"commutators"::: ) "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" )))) ; theorem :: GROUP_5:54 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k5_group_5 :::"commutators"::: ) "(" (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" ) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set ($#k5_group_5 :::"commutators"::: ) "(" (Set (Var "H")) "," (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ")" ))) ; theorem :: GROUP_5:55 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "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 "(" (Bool (Set ($#k5_group_5 :::"commutators"::: ) "(" (Set (Var "H")) "," (Set (Var "N")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "N")))) & (Bool (Set ($#k5_group_5 :::"commutators"::: ) "(" (Set (Var "N")) "," (Set (Var "H")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "N")))) ")" )))) ; theorem :: GROUP_5:56 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "H3")) "," (Set (Var "H4")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H2"))) & (Bool (Set (Var "H3")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H4")))) "holds" (Bool (Set ($#k5_group_5 :::"commutators"::: ) "(" (Set (Var "H1")) "," (Set (Var "H3")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k5_group_5 :::"commutators"::: ) "(" (Set (Var "H2")) "," (Set (Var "H4")) ")" )))) ; theorem :: GROUP_5:57 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::)) "iff" (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k5_group_5 :::"commutators"::: ) "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ")" )) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); func :::"commutators"::: "G" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_5:def 6 (Set ($#k5_group_5 :::"commutators"::: ) "(" (Set "(" ($#k7_group_2 :::"(Omega)."::: ) "G" ")" ) "," (Set "(" ($#k7_group_2 :::"(Omega)."::: ) "G" ")" ) ")" ); end; :: deftheorem defines :::"commutators"::: GROUP_5:def 6 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k6_group_5 :::"commutators"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k5_group_5 :::"commutators"::: ) "(" (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ")" ))); theorem :: GROUP_5:58 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_group_5 :::"commutators"::: ) (Set (Var "G")))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ))) ")" ))) ; theorem :: GROUP_5:59 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::)) "iff" (Bool (Set ($#k6_group_5 :::"commutators"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ")" )) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); func :::"[.":::"A" "," "B":::".]"::: -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" equals :: GROUP_5:def 7 (Set ($#k5_group_4 :::"gr"::: ) (Set "(" ($#k4_group_5 :::"commutators"::: ) "(" "A" "," "B" ")" ")" )); end; :: deftheorem defines :::"[."::: GROUP_5:def 7 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k7_group_5 :::"[."::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set "(" ($#k4_group_5 :::"commutators"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ))))); theorem :: GROUP_5:60 (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")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set ($#k7_group_5 :::"[."::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_group_5 :::".]"::: ) ))))) ; theorem :: GROUP_5:61 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set ($#k7_group_5 :::"[."::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_group_5 :::".]"::: ) )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))(Bool "ex" (Set (Var "I")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "I")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_group_5 :::"commutators"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "F")) ($#k4_group_4 :::"|^"::: ) (Set (Var "I")) ")" ))) ")" ))) ")" )))) ; theorem :: GROUP_5:62 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k7_group_5 :::"[."::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_group_5 :::".]"::: ) ) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set ($#k7_group_5 :::"[."::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k7_group_5 :::".]"::: ) )))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H1", "H2" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); func :::"[.":::"H1" "," "H2":::".]"::: -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" equals :: GROUP_5:def 8 (Set ($#k7_group_5 :::"[."::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) "H1" ")" ) "," (Set "(" ($#k8_group_2 :::"carr"::: ) "H2" ")" ) ($#k7_group_5 :::".]"::: ) ); end; :: deftheorem defines :::"[."::: GROUP_5:def 8 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k8_group_5 :::"[."::: ) (Set (Var "H1")) "," (Set (Var "H2")) ($#k8_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_group_5 :::"[."::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" ) "," (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" ) ($#k7_group_5 :::".]"::: ) )))); theorem :: GROUP_5:63 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k8_group_5 :::"[."::: ) (Set (Var "H1")) "," (Set (Var "H2")) ($#k8_group_5 :::".]"::: ) ) ($#r1_group_2 :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set "(" ($#k5_group_5 :::"commutators"::: ) "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" ")" ))))) ; theorem :: GROUP_5:64 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set ($#k8_group_5 :::"[."::: ) (Set (Var "H1")) "," (Set (Var "H2")) ($#k8_group_5 :::".]"::: ) )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))(Bool "ex" (Set (Var "I")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "I")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_group_5 :::"commutators"::: ) "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "F")) ($#k4_group_4 :::"|^"::: ) (Set (Var "I")) ")" ))) ")" ))) ")" )))) ; theorem :: GROUP_5:65 (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")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1"))) & (Bool (Set (Var "b")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H2")))) "holds" (Bool (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set ($#k8_group_5 :::"[."::: ) (Set (Var "H1")) "," (Set (Var "H2")) ($#k8_group_5 :::".]"::: ) ))))) ; theorem :: GROUP_5:66 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "H3")) "," (Set (Var "H4")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H2"))) & (Bool (Set (Var "H3")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H4")))) "holds" (Bool (Set ($#k8_group_5 :::"[."::: ) (Set (Var "H1")) "," (Set (Var "H3")) ($#k8_group_5 :::".]"::: ) ) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set ($#k8_group_5 :::"[."::: ) (Set (Var "H2")) "," (Set (Var "H4")) ($#k8_group_5 :::".]"::: ) )))) ; theorem :: GROUP_5:67 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "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 "(" (Bool (Set ($#k8_group_5 :::"[."::: ) (Set (Var "N")) "," (Set (Var "H")) ($#k8_group_5 :::".]"::: ) ) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "N"))) & (Bool (Set ($#k8_group_5 :::"[."::: ) (Set (Var "H")) "," (Set (Var "N")) ($#k8_group_5 :::".]"::: ) ) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "N"))) ")" )))) ; theorem :: GROUP_5:68 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k8_group_5 :::"[."::: ) (Set (Var "N1")) "," (Set (Var "N2")) ($#k8_group_5 :::".]"::: ) ) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))))) ; theorem :: GROUP_5:69 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k8_group_5 :::"[."::: ) (Set (Var "N1")) "," (Set (Var "N2")) ($#k8_group_5 :::".]"::: ) ) ($#r1_group_2 :::"="::: ) (Set ($#k8_group_5 :::"[."::: ) (Set (Var "N2")) "," (Set (Var "N1")) ($#k8_group_5 :::".]"::: ) )))) ; theorem :: GROUP_5:70 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "," (Set (Var "N3")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k8_group_5 :::"[."::: ) (Set "(" (Set (Var "N1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "N2")) ")" ) "," (Set (Var "N3")) ($#k8_group_5 :::".]"::: ) ) ($#r1_group_2 :::"="::: ) (Set (Set ($#k8_group_5 :::"[."::: ) (Set (Var "N1")) "," (Set (Var "N3")) ($#k8_group_5 :::".]"::: ) ) ($#k8_group_4 :::""\/""::: ) (Set ($#k8_group_5 :::"[."::: ) (Set (Var "N2")) "," (Set (Var "N3")) ($#k8_group_5 :::".]"::: ) ))))) ; theorem :: GROUP_5:71 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "," (Set (Var "N3")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k8_group_5 :::"[."::: ) (Set (Var "N1")) "," (Set "(" (Set (Var "N2")) ($#k8_group_4 :::""\/""::: ) (Set (Var "N3")) ")" ) ($#k8_group_5 :::".]"::: ) ) ($#r1_group_2 :::"="::: ) (Set (Set ($#k8_group_5 :::"[."::: ) (Set (Var "N1")) "," (Set (Var "N2")) ($#k8_group_5 :::".]"::: ) ) ($#k8_group_4 :::""\/""::: ) (Set ($#k8_group_5 :::"[."::: ) (Set (Var "N1")) "," (Set (Var "N3")) ($#k8_group_5 :::".]"::: ) ))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); func "G" :::"`"::: -> ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" equals :: GROUP_5:def 9 (Set ($#k8_group_5 :::"[."::: ) (Set "(" ($#k7_group_2 :::"(Omega)."::: ) "G" ")" ) "," (Set "(" ($#k7_group_2 :::"(Omega)."::: ) "G" ")" ) ($#k8_group_5 :::".]"::: ) ); end; :: deftheorem defines :::"`"::: GROUP_5:def 9 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set (Set (Var "G")) ($#k9_group_5 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_group_5 :::"[."::: ) (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ($#k8_group_5 :::".]"::: ) ))); theorem :: GROUP_5:72 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set (Set (Var "G")) ($#k9_group_5 :::"`"::: ) ) ($#r1_group_2 :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set "(" ($#k6_group_5 :::"commutators"::: ) (Set (Var "G")) ")" )))) ; theorem :: GROUP_5:73 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "G")) ($#k9_group_5 :::"`"::: ) )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))(Bool "ex" (Set (Var "I")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "I")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_group_5 :::"commutators"::: ) (Set (Var "G")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "F")) ($#k4_group_4 :::"|^"::: ) (Set (Var "I")) ")" ))) ")" ))) ")" ))) ; theorem :: GROUP_5:74 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (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 (Set (Var "G")) ($#k9_group_5 :::"`"::: ) )))) ; theorem :: GROUP_5:75 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::)) "iff" (Bool (Set (Set (Var "G")) ($#k9_group_5 :::"`"::: ) ) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))) ")" )) ; theorem :: GROUP_5:76 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Var "H"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set ($#k18_group_2 :::"index"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool (Set (Set (Var "G")) ($#k9_group_5 :::"`"::: ) ) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H"))))) ; begin definitionlet "G" be ($#l3_algstr_0 :::"Group":::); func :::"center"::: "G" -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" means :: GROUP_5:def 10 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))))) "}" ); end; :: deftheorem defines :::"center"::: GROUP_5:def 10 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "b2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_group_5 :::"center"::: ) (Set (Var "G")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))))) "}" ) ")" ))); theorem :: GROUP_5:77 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set ($#k10_group_5 :::"center"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))))) ")" ))) ; theorem :: GROUP_5:78 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k10_group_5 :::"center"::: ) (Set (Var "G"))) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")))) ; theorem :: GROUP_5:79 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set ($#k10_group_5 :::"center"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "H")) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))))) ; theorem :: GROUP_5:80 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k10_group_5 :::"center"::: ) (Set (Var "G"))) "is" ($#v5_group_1 :::"commutative"::: ) )) ; theorem :: GROUP_5:81 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set ($#k10_group_5 :::"center"::: ) (Set (Var "G")))) "iff" (Bool (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) ")" ))) ; theorem :: GROUP_5:82 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::)) "iff" (Bool (Set ($#k10_group_5 :::"center"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))) ")" )) ;