:: GROUP_2 semantic presentation begin theorem :: GROUP_2:1 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v8_struct_0 :::"finite"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) ))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); func "A" :::"""::: -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_2:def 1 "{" (Set "(" (Set (Var "g")) ($#k2_group_1 :::"""::: ) ")" ) where g "is" ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) "A") "}" ; involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "g")) ($#k2_group_1 :::"""::: ) ")" ) where g "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")) : (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "}" )) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "g")) ($#k2_group_1 :::"""::: ) ")" ) where g "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")) : (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "}" )) ; end; :: deftheorem defines :::"""::: GROUP_2:def 1 : (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 (Set (Set (Var "A")) ($#k1_group_2 :::"""::: ) ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "g")) ($#k2_group_1 :::"""::: ) ")" ) where g "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" ))); theorem :: GROUP_2:2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (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 (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k1_group_2 :::"""::: ) )) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k2_group_1 :::"""::: ) )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" )))) ; theorem :: GROUP_2:3 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "g")) ($#k6_domain_1 :::"}"::: ) ) ($#k1_group_2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "g")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: GROUP_2:4 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "g")) "," (Set (Var "h")) ($#k7_domain_1 :::"}"::: ) ) ($#k1_group_2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set "(" (Set (Var "g")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set "(" (Set (Var "h")) ($#k2_group_1 :::"""::: ) ")" ) ($#k7_domain_1 :::"}"::: ) )))) ; theorem :: GROUP_2:5 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" ) ($#k1_group_2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: GROUP_2:6 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" ) ($#k1_group_2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))))) ; theorem :: GROUP_2:7 (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 (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set (Set (Var "A")) ($#k1_group_2 :::"""::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; registrationlet "G" be ($#l3_algstr_0 :::"Group":::); let "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); cluster (Set "A" ($#k1_group_2 :::"""::: ) ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "G" be ($#l3_algstr_0 :::"Group":::); let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); cluster (Set "A" ($#k1_group_2 :::"""::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); func "A" :::"*"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_2:def 2 "{" (Set "(" (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")) ")" ) where g, h "is" ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool "(" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) "B") ")" ) "}" ; end; :: deftheorem defines :::"*"::: GROUP_2:def 2 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")) ")" ) where g, h "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool "(" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" ))); definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); :: original: :::"*"::: redefine func "A" :::"*"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "G"; commutativity (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")) "holds" (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k2_group_2 :::"*"::: ) (Set (Var "A"))))) ; end; theorem :: GROUP_2:8 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (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 (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")))) "iff" (Bool "ex" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" )) ")" )))) ; theorem :: GROUP_2:9 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "iff" (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: GROUP_2:10 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_group_1 :::"associative"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k2_group_2 :::"*"::: ) (Set (Var "C")) ")" ))))) ; theorem :: GROUP_2:11 (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 (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")) ")" ) ($#k1_group_2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k1_group_2 :::"""::: ) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k1_group_2 :::"""::: ) ")" ))))) ; theorem :: GROUP_2:12 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k1_finsub_1 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")) ")" ) ($#k1_finsub_1 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "C")) ")" ))))) ; theorem :: GROUP_2:13 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_finsub_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "C")) ")" ) ($#k1_finsub_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k2_group_2 :::"*"::: ) (Set (Var "C")) ")" ))))) ; theorem :: GROUP_2:14 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k3_finsub_1 :::"/\"::: ) (Set (Var "C")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")) ")" ) ($#k3_finsub_1 :::"/\"::: ) (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "C")) ")" ))))) ; theorem :: GROUP_2:15 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k3_finsub_1 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "C")) ")" ) ($#k3_finsub_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k2_group_2 :::"*"::: ) (Set (Var "C")) ")" ))))) ; theorem :: GROUP_2:16 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: GROUP_2:17 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) ")" ))) ; theorem :: GROUP_2:18 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "g")) ($#k6_domain_1 :::"}"::: ) ) ($#k2_group_2 :::"*"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "h")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: GROUP_2:19 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "g")) ($#k6_domain_1 :::"}"::: ) ) ($#k2_group_2 :::"*"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "g1")) "," (Set (Var "g2")) ($#k7_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set "(" (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g1")) ")" ) "," (Set "(" (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2")) ")" ) ($#k7_domain_1 :::"}"::: ) )))) ; theorem :: GROUP_2:20 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "g1")) "," (Set (Var "g2")) ($#k7_domain_1 :::"}"::: ) ) ($#k2_group_2 :::"*"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "g")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set "(" (Set (Var "g1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "g2")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g")) ")" ) ($#k7_domain_1 :::"}"::: ) )))) ; theorem :: GROUP_2:21 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "g")) "," (Set (Var "h")) ($#k7_domain_1 :::"}"::: ) ) ($#k2_group_2 :::"*"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "g1")) "," (Set (Var "g2")) ($#k7_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_domain_1 :::"{"::: ) (Set "(" (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g1")) ")" ) "," (Set "(" (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2")) ")" ) "," (Set "(" (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g1")) ")" ) "," (Set "(" (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2")) ")" ) ($#k9_domain_1 :::"}"::: ) )))) ; theorem :: GROUP_2:22 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool "(" "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "g2")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "g1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "g")) ($#k2_group_1 :::"""::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: GROUP_2:23 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "g")) ($#k2_group_1 :::"""::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k1_group_2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: GROUP_2:24 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "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 (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k2_group_2 :::"*"::: ) (Set (Var "A")))))) ; theorem :: GROUP_2:25 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::))) "holds" (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k2_group_2 :::"*"::: ) (Set (Var "A")))))) ; theorem :: GROUP_2:26 (Bool "for" (Set (Var "G")) "being" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k3_group_2 :::"*"::: ) (Set (Var "B")) ")" ) ($#k1_group_2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_group_2 :::"""::: ) ")" ) ($#k3_group_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k1_group_2 :::"""::: ) ")" ))))) ; definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "g" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); func "g" :::"*"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_2:def 3 (Set (Set ($#k6_domain_1 :::"{"::: ) "g" ($#k6_domain_1 :::"}"::: ) ) ($#k2_group_2 :::"*"::: ) "A"); func "A" :::"*"::: "g" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_2:def 4 (Set "A" ($#k2_group_2 :::"*"::: ) (Set ($#k6_domain_1 :::"{"::: ) "g" ($#k6_domain_1 :::"}"::: ) )); end; :: deftheorem defines :::"*"::: GROUP_2:def 3 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "g")) ($#k4_group_2 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "g")) ($#k6_domain_1 :::"}"::: ) ) ($#k2_group_2 :::"*"::: ) (Set (Var "A"))))))); :: deftheorem defines :::"*"::: GROUP_2:def 4 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "A")) ($#k5_group_2 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "g")) ($#k6_domain_1 :::"}"::: ) )))))); theorem :: GROUP_2:27 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "g")) ($#k4_group_2 :::"*"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")))) & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" ))))) ; theorem :: GROUP_2:28 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k5_group_2 :::"*"::: ) (Set (Var "g")))) "iff" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g")))) & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" ))))) ; theorem :: GROUP_2:29 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_group_1 :::"associative"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k4_group_2 :::"*"::: ) (Set (Var "A")) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k4_group_2 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")) ")" )))))) ; theorem :: GROUP_2:30 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_group_1 :::"associative"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k5_group_2 :::"*"::: ) (Set (Var "g")) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k4_group_2 :::"*"::: ) (Set (Var "B")) ")" )))))) ; theorem :: GROUP_2:31 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_group_1 :::"associative"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")) ")" ) ($#k5_group_2 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k5_group_2 :::"*"::: ) (Set (Var "g")) ")" )))))) ; theorem :: GROUP_2:32 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_group_1 :::"associative"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")) ")" ) ($#k4_group_2 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k4_group_2 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k4_group_2 :::"*"::: ) (Set (Var "A")) ")" )))))) ; theorem :: GROUP_2:33 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_group_1 :::"associative"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k4_group_2 :::"*"::: ) (Set (Var "A")) ")" ) ($#k5_group_2 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k4_group_2 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k5_group_2 :::"*"::: ) (Set (Var "h")) ")" )))))) ; theorem :: GROUP_2:34 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_group_1 :::"associative"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k5_group_2 :::"*"::: ) (Set (Var "g")) ")" ) ($#k5_group_2 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_group_2 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")) ")" )))))) ; theorem :: GROUP_2:35 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" ) ($#k5_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "a")) ($#k4_group_2 :::"*"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: GROUP_2:36 (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 (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" ) ($#k5_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set (Set (Var "a")) ($#k4_group_2 :::"*"::: ) (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) ")" ))) ; theorem :: GROUP_2:37 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k4_group_2 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "A")) ($#k5_group_2 :::"*"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" ))) ; theorem :: GROUP_2:38 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::))) "holds" (Bool (Set (Set (Var "g")) ($#k4_group_2 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_group_2 :::"*"::: ) (Set (Var "g"))))))) ; definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; mode :::"Subgroup"::: "of" "G" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) means :: GROUP_2:def 5 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G")) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G") ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) ")" ); end; :: deftheorem defines :::"Subgroup"::: GROUP_2:def 5 : (Bool "for" (Set (Var "G")) "," (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) ")" ) ")" )); theorem :: GROUP_2:39 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v8_struct_0 :::"finite"::: ) )) "holds" (Bool (Set (Var "H")) "is" ($#v8_struct_0 :::"finite"::: ) ))) ; theorem :: GROUP_2:40 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "G")))))) ; theorem :: GROUP_2:41 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set (Var "h")) ($#r1_struct_0 :::"in"::: ) (Set (Var "G")))))) ; theorem :: GROUP_2:42 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set (Var "h")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")))))) ; theorem :: GROUP_2:43 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "h1")) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "h2")) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool (Set (Set (Var "h1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2")))))))) ; registrationlet "G" be ($#l3_algstr_0 :::"Group":::); cluster -> ($#v3_group_1 :::"associative"::: ) for ($#m1_group_2 :::"Subgroup"::: ) "of" "G"; end; theorem :: GROUP_2:44 (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 (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; theorem :: GROUP_2:45 (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 "H1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "H2")))))) ; theorem :: GROUP_2:46 (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 (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))))) ; theorem :: GROUP_2:47 (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 "H1"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "H2"))))) ; theorem :: GROUP_2:48 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool (Set (Set (Var "h")) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k2_group_1 :::"""::: ) )))))) ; theorem :: GROUP_2:49 (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 (Set ($#k3_group_1 :::"inverse_op"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_group_1 :::"inverse_op"::: ) (Set (Var "G")) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))))))) ; theorem :: GROUP_2:50 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "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 "g1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) & (Bool (Set (Var "g2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))) "holds" (Bool (Set (Set (Var "g1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))))) ; theorem :: GROUP_2:51 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "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 "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))) "holds" (Bool (Set (Set (Var "g")) ($#k2_group_1 :::"""::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))))) ; registrationlet "G" be ($#l3_algstr_0 :::"Group":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) for ($#m1_group_2 :::"Subgroup"::: ) "of" "G"; end; theorem :: GROUP_2:52 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "g2")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "g1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "g")) ($#k2_group_1 :::"""::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) "holds" (Bool "ex" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))))) ; theorem :: GROUP_2:53 (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 "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::))) "holds" (Bool (Set (Var "H")) "is" ($#v5_group_1 :::"commutative"::: ) ))) ; registrationlet "G" be ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::); cluster -> ($#v5_group_1 :::"commutative"::: ) for ($#m1_group_2 :::"Subgroup"::: ) "of" "G"; end; theorem :: GROUP_2:54 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set (Var "G")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")))) ; theorem :: GROUP_2:55 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "G1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G2"))) & (Bool (Set (Var "G2")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G1")))) "holds" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G1"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G2"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G2"))) "#)" ))) ; theorem :: GROUP_2:56 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "G1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G2"))) & (Bool (Set (Var "G2")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G3")))) "holds" (Bool (Set (Var "G1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G3")))) ; theorem :: GROUP_2:57 (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 "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))) "holds" (Bool (Set (Var "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H2"))))) ; theorem :: GROUP_2:58 (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 "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1")))) "holds" (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H2"))) ")" )) "holds" (Bool (Set (Var "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H2"))))) ; theorem :: GROUP_2:59 (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 "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))) "holds" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H2"))) "#)" )))) ; theorem :: GROUP_2:60 (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 "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1"))) "iff" (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H2"))) ")" ) ")" )) "holds" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H2"))) "#)" )))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H1", "H2" be ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); :: original: :::"="::: redefine pred "H1" :::"="::: "H2" means :: GROUP_2:def 6 (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) "H1") "iff" (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) "H2") ")" )); end; :: deftheorem defines :::"="::: GROUP_2:def 6 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H1")) ($#r1_group_2 :::"="::: ) (Set (Var "H2"))) "iff" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1"))) "iff" (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H2"))) ")" )) ")" ))); theorem :: GROUP_2:61 (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 "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))))) "holds" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "#)" )))) ; theorem :: GROUP_2:62 (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 "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) ")" )) "holds" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "#)" )))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); func :::"(1)."::: "G" -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" means :: GROUP_2:def 7 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) "G" ")" ) ($#k6_domain_1 :::"}"::: ) )); end; :: deftheorem defines :::"(1)."::: GROUP_2:def 7 : (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 ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#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 :::"(Omega)."::: "G" -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" equals :: GROUP_2:def 8 (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G") "#)" ); projectivity (Bool "for" (Set (Var "b1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")) (Bool "for" (Set (Var "b2")) "being" ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b2"))) "#)" ))) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b1"))) "#)" )))) ; end; :: deftheorem defines :::"(Omega)."::: GROUP_2:def 8 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "#)" ))); theorem :: GROUP_2:63 (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 (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))))) ; theorem :: GROUP_2:64 (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 ($#k6_group_2 :::"(1)."::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "H2")))))) ; theorem :: GROUP_2:65 (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 (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G"))) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H"))))) ; theorem :: GROUP_2:66 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Var "H")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")))))) ; theorem :: GROUP_2:67 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set (Var "G")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G"))))) ; theorem :: GROUP_2:68 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G"))) "is" ($#v8_struct_0 :::"finite"::: ) )) ; registrationlet "G" be ($#l3_algstr_0 :::"Group":::); cluster (Set ($#k6_group_2 :::"(1)."::: ) "G") -> ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) for ($#m1_group_2 :::"Subgroup"::: ) "of" "G"; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; registrationlet "G" be ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::); cluster -> ($#v8_struct_0 :::"finite"::: ) for ($#m1_group_2 :::"Subgroup"::: ) "of" "G"; end; theorem :: GROUP_2:69 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k7_group_1 :::"card"::: ) (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: GROUP_2:70 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Var "H")) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))))) ; theorem :: GROUP_2:71 (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 (Set ($#k7_struct_0 :::"card"::: ) (Set (Var "H"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k7_struct_0 :::"card"::: ) (Set (Var "G")))))) ; theorem :: GROUP_2:72 (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "H"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G")))))) ; theorem :: GROUP_2:73 (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k7_group_1 :::"card"::: ) (Set (Var "H"))))) "holds" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "#)" )))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); func :::"carr"::: "H" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_2:def 9 (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "H"); end; :: deftheorem defines :::"carr"::: GROUP_2:def 9 : (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 (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H")))))); theorem :: GROUP_2:74 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "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 "g1")) ($#r2_hidden :::"in"::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H")))) & (Bool (Set (Var "g2")) ($#r2_hidden :::"in"::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Set (Var "g1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))))))) ; theorem :: GROUP_2:75 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "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 "g")) ($#r2_hidden :::"in"::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Set (Var "g")) ($#k2_group_1 :::"""::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))))))) ; theorem :: GROUP_2:76 (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 (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H")))))) ; theorem :: GROUP_2:77 (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 (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H")) ")" ) ($#k1_group_2 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H")))))) ; theorem :: GROUP_2:78 (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 (Bool (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" )))) "implies" (Bool "ex" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" )))) ")" & "(" (Bool (Bool "ex" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" ))))) "implies" (Bool (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" ))) ")" ")" ))) ; theorem :: GROUP_2:79 (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 "ex" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" )))))) ; 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" means :: GROUP_2:def 10 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) "H1" ")" ) ($#k3_finsub_1 :::"/\"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) "H2" ")" ))); end; :: deftheorem defines :::"/\"::: GROUP_2:def 10 : (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")) (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 (Set (Var "H1")) ($#k9_group_2 :::"/\"::: ) (Set (Var "H2")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k3_finsub_1 :::"/\"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" ))) ")" )))); theorem :: GROUP_2:80 (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 "(" "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k9_group_2 :::"/\"::: ) (Set (Var "H2"))))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))) ")" ) & (Bool "(" "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2")))))) "holds" (Bool (Set (Var "H")) ($#r1_group_2 :::"="::: ) (Set (Set (Var "H1")) ($#k9_group_2 :::"/\"::: ) (Set (Var "H2")))) ")" ) ")" ))) ; theorem :: GROUP_2:81 (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_2 :::"carr"::: ) (Set "(" (Set (Var "H1")) ($#k9_group_2 :::"/\"::: ) (Set (Var "H2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k3_finsub_1 :::"/\"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" ))))) ; theorem :: GROUP_2:82 (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 (Set (Var "H1")) ($#k9_group_2 :::"/\"::: ) (Set (Var "H2")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1"))) & (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H2"))) ")" ) ")" )))) ; theorem :: GROUP_2:83 (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")) "holds" (Bool (Set (Set (Var "H")) ($#k9_group_2 :::"/\"::: ) (Set (Var "H"))) ($#r1_group_2 :::"="::: ) (Set (Var "H"))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H1", "H2" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); :: original: :::"/\"::: redefine func "H1" :::"/\"::: "H2" -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G"; commutativity (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")) "holds" (Bool (Set (Set (Var "H1")) ($#k9_group_2 :::"/\"::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H2")) ($#k9_group_2 :::"/\"::: ) (Set (Var "H1"))))) ; end; theorem :: GROUP_2:84 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "H3")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2")) ")" ) ($#k10_group_2 :::"/\"::: ) (Set (Var "H3"))) ($#r1_group_2 :::"="::: ) (Set (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set "(" (Set (Var "H2")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H3")) ")" ))))) ; theorem :: GROUP_2:85 (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 (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" ) ($#k10_group_2 :::"/\"::: ) (Set (Var "H"))) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "H")) ($#k10_group_2 :::"/\"::: ) (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" )) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))) ")" ))) ; theorem :: GROUP_2:86 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "H")) ($#k10_group_2 :::"/\"::: ) (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" )) ($#r1_group_2 :::"="::: ) (Set (Var "H"))) & (Bool (Set (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ($#k10_group_2 :::"/\"::: ) (Set (Var "H"))) ($#r1_group_2 :::"="::: ) (Set (Var "H"))) ")" ))) ; theorem :: GROUP_2:87 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ($#k10_group_2 :::"/\"::: ) (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "G")))) ; theorem :: GROUP_2:88 (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 (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2"))) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H1"))) & (Bool (Set (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2"))) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H2"))) ")" ))) ; theorem :: GROUP_2:89 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H2")) "," (Set (Var "H1")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H2"))) "iff" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2")) ")" )) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set "(" (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2")) ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H1"))) "#)" )) ")" ))) ; theorem :: GROUP_2:90 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "H3")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H2")))) "holds" (Bool (Set (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H3"))) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H2"))))) ; theorem :: GROUP_2:91 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "H3")) "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 "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H3")))) "holds" (Bool (Set (Var "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Set (Var "H2")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H3")))))) ; theorem :: GROUP_2:92 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "H3")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H2")))) "holds" (Bool (Set (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H3"))) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Set (Var "H2")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H3")))))) ; theorem :: GROUP_2:93 (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 "(" (Bool (Set (Var "H1")) "is" ($#v8_struct_0 :::"finite"::: ) ) "or" (Bool (Set (Var "H2")) "is" ($#v8_struct_0 :::"finite"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2"))) "is" ($#v8_struct_0 :::"finite"::: ) ))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); func "A" :::"*"::: "H" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_2:def 11 (Set "A" ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) "H" ")" )); func "H" :::"*"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_2:def 12 (Set (Set "(" ($#k8_group_2 :::"carr"::: ) "H" ")" ) ($#k2_group_2 :::"*"::: ) "A"); end; :: deftheorem defines :::"*"::: GROUP_2:def 11 : (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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "A")) ($#k11_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H")) ")" )))))); :: deftheorem defines :::"*"::: GROUP_2:def 12 : (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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H")) ($#k12_group_2 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H")) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "A"))))))); theorem :: GROUP_2:94 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k11_group_2 :::"*"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2")))) & (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "g2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) ")" )) ")" ))))) ; theorem :: GROUP_2:95 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "H")) ($#k12_group_2 :::"*"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2")))) & (Bool (Set (Var "g1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) & (Bool (Set (Var "g2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" ))))) ; theorem :: GROUP_2:96 (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")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")) ")" ) ($#k11_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k11_group_2 :::"*"::: ) (Set (Var "H")) ")" )))))) ; theorem :: GROUP_2:97 (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")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k11_group_2 :::"*"::: ) (Set (Var "H")) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "H")) ($#k12_group_2 :::"*"::: ) (Set (Var "B")) ")" )))))) ; theorem :: GROUP_2:98 (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")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "H")) ($#k12_group_2 :::"*"::: ) (Set (Var "A")) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k12_group_2 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")) ")" )))))) ; theorem :: GROUP_2:99 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k11_group_2 :::"*"::: ) (Set (Var "H1")) ")" ) ($#k11_group_2 :::"*"::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "H1")) ($#k12_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" ) ")" )))))) ; theorem :: GROUP_2:100 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "H1")) ($#k12_group_2 :::"*"::: ) (Set (Var "A")) ")" ) ($#k11_group_2 :::"*"::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k12_group_2 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k11_group_2 :::"*"::: ) (Set (Var "H2")) ")" )))))) ; theorem :: GROUP_2:101 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "H1")) ($#k12_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" ) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k12_group_2 :::"*"::: ) (Set "(" (Set (Var "H2")) ($#k12_group_2 :::"*"::: ) (Set (Var "A")) ")" )))))) ; theorem :: GROUP_2:102 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "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 (Set (Set (Var "A")) ($#k11_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k12_group_2 :::"*"::: ) (Set (Var "A"))))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func "a" :::"*"::: "H" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_2:def 13 (Set "a" ($#k4_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) "H" ")" )); func "H" :::"*"::: "a" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_2:def 14 (Set (Set "(" ($#k8_group_2 :::"carr"::: ) "H" ")" ) ($#k5_group_2 :::"*"::: ) "a"); end; :: deftheorem defines :::"*"::: GROUP_2:def 13 : (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 "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H")) ")" )))))); :: deftheorem defines :::"*"::: GROUP_2:def 14 : (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 "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H")) ")" ) ($#k5_group_2 :::"*"::: ) (Set (Var "a"))))))); theorem :: GROUP_2:103 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (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 "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "g")) "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 "g")))) & (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) ")" )) ")" ))))) ; theorem :: GROUP_2:104 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (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 "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")))) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")))) & (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) ")" )) ")" ))))) ; theorem :: GROUP_2:105 (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")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_group_2 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")) ")" )))))) ; theorem :: GROUP_2:106 (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")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")) ")" ) ($#k5_group_2 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_group_2 :::"*"::: ) (Set "(" (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "b")) ")" )))))) ; theorem :: GROUP_2:107 (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")) "holds" (Bool (Set (Set "(" (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k5_group_2 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" )))))) ; theorem :: GROUP_2:108 (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 "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")))) ")" )))) ; theorem :: GROUP_2:109 (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 (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H")))) & (Bool (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H")))) ")" ))) ; theorem :: GROUP_2:110 (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 (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" ) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) ")" ))) ; theorem :: GROUP_2:111 (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 (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) ")" ))) ; theorem :: GROUP_2:112 (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 "H")) "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 (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))))))) ; theorem :: GROUP_2:113 (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 "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) "iff" (Bool (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H")))) ")" )))) ; theorem :: GROUP_2:114 (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")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")))) "iff" (Bool (Set (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) ")" )))) ; theorem :: GROUP_2:115 (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")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")))) "iff" (Bool (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "b")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")))) ")" )))) ; theorem :: GROUP_2:116 (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")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")) ")" )))))) ; theorem :: GROUP_2:117 (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 "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k13_group_2 :::"*"::: ) (Set (Var "H")) ")" ))) & (Bool (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k13_group_2 :::"*"::: ) (Set (Var "H")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")) ")" ))) ")" )))) ; theorem :: GROUP_2:118 (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 "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Num 2) ")" ) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")) ")" )))))) ; theorem :: GROUP_2:119 (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 "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) "iff" (Bool (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H")))) ")" )))) ; theorem :: GROUP_2:120 (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")) "holds" (Bool "(" (Bool (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "b")))) "iff" (Bool (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" )) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) ")" )))) ; theorem :: GROUP_2:121 (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")) "holds" (Bool "(" (Bool (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "b")))) "iff" (Bool (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "b")))) ")" )))) ; theorem :: GROUP_2:122 (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")) "holds" (Bool (Set (Set "(" (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k5_group_2 :::"*"::: ) (Set (Var "b"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "b")) ")" )))))) ; theorem :: GROUP_2:123 (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 "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ")" ))) & (Bool (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" ))) ")" )))) ; theorem :: GROUP_2:124 (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 "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Num 2) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" )))))) ; theorem :: GROUP_2:125 (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 "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set "(" (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H1")) ")" ) ($#k3_finsub_1 :::"/\"::: ) (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H2")) ")" )))))) ; theorem :: GROUP_2:126 (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 "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2")) ")" ) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "H1")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_finsub_1 :::"/\"::: ) (Set "(" (Set (Var "H2")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" )))))) ; theorem :: GROUP_2:127 (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 "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "H1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H2")) ")" ) ($#k5_group_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ))))))) ; theorem :: GROUP_2:128 (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")) "holds" (Bool (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) "," (Set (Set (Var "b")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r2_wellord2 :::"are_equipotent"::: ) )))) ; theorem :: GROUP_2:129 (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")) "holds" (Bool (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) "," (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "b"))) ($#r2_wellord2 :::"are_equipotent"::: ) )))) ; theorem :: GROUP_2:130 (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")) "holds" (Bool (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))) "," (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "b"))) ($#r2_wellord2 :::"are_equipotent"::: ) )))) ; theorem :: GROUP_2:131 (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 "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))) "," (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r2_wellord2 :::"are_equipotent"::: ) ) & (Bool (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))) "," (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))) ($#r2_wellord2 :::"are_equipotent"::: ) ) ")" )))) ; theorem :: GROUP_2:132 (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 "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k7_struct_0 :::"card"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")) ")" ))) & (Bool (Set ($#k7_struct_0 :::"card"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" ))) ")" )))) ; theorem :: GROUP_2:133 (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 "H")) "being" ($#v8_struct_0 :::"finite"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "B")) "," (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")))) & (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")))) & (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B")))) & (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C")))) ")" ))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); func :::"Left_Cosets"::: "H" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "G" means :: GROUP_2:def 15 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "G" "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) "H"))) ")" )); func :::"Right_Cosets"::: "H" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "G" means :: GROUP_2:def 16 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "G" "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "H" ($#k14_group_2 :::"*"::: ) (Set (Var "a"))))) ")" )); end; :: deftheorem defines :::"Left_Cosets"::: GROUP_2:def 15 : (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 "b3")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Var "H")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))))) ")" )) ")" )))); :: deftheorem defines :::"Right_Cosets"::: GROUP_2:def 16 : (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 "b3")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k16_group_2 :::"Right_Cosets"::: ) (Set (Var "H")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))))) ")" )) ")" )))); theorem :: GROUP_2:134 (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 "G")) "is" ($#v8_struct_0 :::"finite"::: ) )) "holds" (Bool "(" (Bool (Set ($#k16_group_2 :::"Right_Cosets"::: ) (Set (Var "H"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Var "H"))) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ))) ; theorem :: GROUP_2:135 (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 ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Var "H")))) & (Bool (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))) ($#r2_hidden :::"in"::: ) (Set ($#k16_group_2 :::"Right_Cosets"::: ) (Set (Var "H")))) ")" ))) ; theorem :: GROUP_2:136 (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 (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Var "H"))) "," (Set ($#k16_group_2 :::"Right_Cosets"::: ) (Set (Var "H"))) ($#r2_wellord2 :::"are_equipotent"::: ) ))) ; theorem :: GROUP_2:137 (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_setfam_1 :::"union"::: ) (Set "(" ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k16_group_2 :::"Right_Cosets"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) ")" ))) ; theorem :: GROUP_2:138 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool verum) "}" )) ; theorem :: GROUP_2:139 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k16_group_2 :::"Right_Cosets"::: ) (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool verum) "}" )) ; theorem :: GROUP_2:140 (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"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool verum) "}" )) "holds" (Bool (Set (Var "H")) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))))) ; theorem :: GROUP_2:141 (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 ($#k16_group_2 :::"Right_Cosets"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool verum) "}" )) "holds" (Bool (Set (Var "H")) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))))) ; theorem :: GROUP_2:142 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k16_group_2 :::"Right_Cosets"::: ) (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ($#k1_tarski :::"}"::: ) )) ")" )) ; theorem :: GROUP_2:143 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#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"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "G"))))) ; theorem :: GROUP_2:144 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#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 ($#k16_group_2 :::"Right_Cosets"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "G"))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); func :::"Index"::: "H" -> ($#m1_hidden :::"Cardinal":::) equals :: GROUP_2:def 17 (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k15_group_2 :::"Left_Cosets"::: ) "H" ")" )); end; :: deftheorem defines :::"Index"::: GROUP_2:def 17 : (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 (Set ($#k17_group_2 :::"Index"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Var "H")) ")" ))))); theorem :: GROUP_2:145 (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 ($#k17_group_2 :::"Index"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Var "H")) ")" ))) & (Bool (Set ($#k17_group_2 :::"Index"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k16_group_2 :::"Right_Cosets"::: ) (Set (Var "H")) ")" ))) ")" ))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); assume (Bool (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Const "H"))) "is" ($#v1_finset_1 :::"finite"::: ) ) ; func :::"index"::: "H" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GROUP_2:def 18 (Bool "ex" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k15_group_2 :::"Left_Cosets"::: ) "H")) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B")))) ")" )); end; :: deftheorem defines :::"index"::: GROUP_2:def 18 : (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 ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Var "H"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k18_group_2 :::"index"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Var "H")))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B")))) ")" )) ")" )))); theorem :: GROUP_2:146 (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 ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Var "H"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool "(" (Bool "ex" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Var "H")))) & (Bool (Set ($#k18_group_2 :::"index"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B")))) ")" )) & (Bool "ex" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k16_group_2 :::"Right_Cosets"::: ) (Set (Var "H")))) & (Bool (Set ($#k18_group_2 :::"index"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C")))) ")" )) ")" ))) ; theorem :: GROUP_2:147 (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_group_1 :::"card"::: ) (Set (Var "H")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k18_group_2 :::"index"::: ) (Set (Var "H")) ")" ))))) ; theorem :: GROUP_2:148 (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "H"))) ($#r1_nat_d :::"divides"::: ) (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G")))))) ; theorem :: GROUP_2:149 (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "I")) "," (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "J")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Var "J")))) "holds" (Bool (Set ($#k18_group_2 :::"index"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_group_2 :::"index"::: ) (Set (Var "J")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k18_group_2 :::"index"::: ) (Set (Var "H")) ")" )))))) ; theorem :: GROUP_2:150 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k18_group_2 :::"index"::: ) (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: GROUP_2:151 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#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 1))) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "G"))))) ; theorem :: GROUP_2:152 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k17_group_2 :::"Index"::: ) (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_struct_0 :::"card"::: ) (Set (Var "G"))))) ; theorem :: GROUP_2:153 (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k18_group_2 :::"index"::: ) (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G"))))) ; theorem :: GROUP_2:154 (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#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 ($#k18_group_2 :::"index"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "H")) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))))) ; theorem :: GROUP_2:155 (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 ($#k17_group_2 :::"Index"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k7_struct_0 :::"card"::: ) (Set (Var "G"))))) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v8_struct_0 :::"finite"::: ) ) & (Bool (Set (Var "H")) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))) ")" ))) ; theorem :: GROUP_2:156 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Var "Y")) "," (Set (Var "Z")) ($#r2_wellord2 :::"are_equipotent"::: ) ) & (Bool (Set (Var "Y")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Z"))) ")" ) ")" ) ")" )) ")" )) "holds" (Bool "ex" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "X")))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k3_nat_1 :::"*"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ))) ")" )))) ;