:: GROUP_8  semantic presentation begin  




















theorem :: GROUP_8:1 (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )     ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Var "p")))) "holds"  (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set   ($#k6_group_1 :::"ord"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "p")))))) ; 
 
theorem :: GROUP_8:2 (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 "a1")) "," (Set (Var "a2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H"))  (Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "a1"))  ($#r1_hidden :::"="::: )  (Set (Var "b1"))) & (Bool (Set (Var "a2"))  ($#r1_hidden :::"="::: )  (Set (Var "b2")))) "holds"  (Bool (Set (Set (Var "a1"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b1"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b2")))))))) ; 
 
theorem :: GROUP_8:3 (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 "H"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k5_group_1 :::"|^"::: )  (Set (Var "n"))))))))) ; 
 
theorem :: GROUP_8:4 (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 "H"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k5_group_1 :::"|^"::: )  (Set (Var "i"))))))))) ; 
 
theorem :: GROUP_8:5 (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 "H"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "G")) "is"   ($#v8_struct_0 :::"finite"::: )  )) "holds"  (Bool (Set   ($#k6_group_1 :::"ord"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_group_1 :::"ord"::: )  (Set (Var "b")))))))) ; 
 
theorem :: GROUP_8:6 (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 "h")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "h"))  ($#r1_struct_0 :::"in"::: )  (Set (Var "H")))) "holds"  (Bool (Set (Set (Var "H"))  ($#k14_group_2 :::"*"::: )  (Set (Var "h")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "H"))))))) ; 
 
theorem :: GROUP_8:7 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k5_group_4 :::"gr"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_group_2 :::"(1)."::: )  (Set (Var "G")))))) ; 
 
theorem :: GROUP_8:8 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Var "G")) ")" )  ($#k5_group_1 :::"|^"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "G")))))) ; 
 
theorem :: GROUP_8:9 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set  "(" (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k6_group_1 :::"ord"::: )  (Set (Var "a")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "G"))))))) ; 
 
theorem :: GROUP_8:10 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "is"   ($#v4_group_1 :::"being_of_order_0"::: )  ))) "holds"  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set  "(" (Set (Var "m"))  ($#k6_int_1 :::"mod"::: )  (Set  "("  ($#k6_group_1 :::"ord"::: )  (Set (Var "a")) ")" ) ")" )))))) ; 
 
theorem :: GROUP_8:11 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Bool  "not" (Set (Var "b")) "is"   ($#v4_group_1 :::"being_of_order_0"::: )  ))) "holds"  (Bool (Set   ($#k5_group_4 :::"gr"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "b")) ($#k6_domain_1 :::"}"::: ) )) "is"   ($#v8_struct_0 :::"finite"::: )  ))) ; 
 
theorem :: GROUP_8:12 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "b")) "is"   ($#v4_group_1 :::"being_of_order_0"::: )  )) "holds"  (Bool (Set (Set (Var "b"))  ($#k2_group_1 :::"""::: )  ) "is"   ($#v4_group_1 :::"being_of_order_0"::: )  ))) ; 
 
theorem :: GROUP_8:13 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "b")) "is"   ($#v4_group_1 :::"being_of_order_0"::: )  ) "iff" (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Set (Var "b"))  ($#k5_group_1 :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "G"))))) "holds"  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))  ")" ))) ; 
 
theorem :: GROUP_8:14 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "G")))))) "holds"  (Bool  "("  (Bool  "("   "for" (Set (Var "H")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  "holds"  (Bool  "("  (Bool (Set (Var "H"))  ($#r1_hidden :::"="::: )  (Set (Var "G"))) "or" (Bool (Set (Var "H"))  ($#r1_group_2 :::"="::: )  (Set   ($#k6_group_2 :::"(1)."::: )  (Set (Var "G"))))  ")" )  ")" ) "iff" (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v1_gr_cy_1 :::"cyclic"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v8_struct_0 :::"finite"::: )  ) & (Bool  "ex" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k7_struct_0 :::"card"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) & (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  )  ")" ))  ")" )  ")" )) ; 
 
theorem :: GROUP_8:15 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "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  "("  (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Set  "(" (Set (Var "x"))  ($#k4_group_2 :::"*"::: )  (Set (Var "A")) ")" )  ($#k5_group_2 :::"*"::: )  (Set (Var "y")))) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "y")))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" ))  ")" )))) ; 
 
theorem :: GROUP_8:16 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k2_group_1 :::"""::: )  ")" )  ($#k4_group_2 :::"*"::: )  (Set (Var "A")) ")" )  ($#k5_group_2 :::"*"::: )  (Set (Var "x")) ")" )))))) ; 
 definitionlet "G" be   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::); let "H", "K" be   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); func  :::"Double_Cosets":::  "(" "H" "," "K" ")"  ->   ($#m1_subset_1 :::"Subset-Family":::) "of" "G" means :: GROUP_8:def 1 (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  "(" "H"  ($#k14_group_2 :::"*"::: )  (Set (Var "a")) ")" )  ($#k11_group_2 :::"*"::: )  "K")))  ")" )); end; 







:: deftheorem    defines :::"Double_Cosets"::: GROUP_8:def 1 :  (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "H")) "," (Set (Var "K")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_8 :::"Double_Cosets"::: )   "(" (Set (Var "H")) "," (Set (Var "K")) ")" )) "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 "b4"))) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "H"))  ($#k14_group_2 :::"*"::: )  (Set (Var "a")) ")" )  ($#k11_group_2 :::"*"::: )  (Set (Var "K")))))  ")" ))  ")" )))); 
 
theorem :: GROUP_8:17 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "z")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "H")) "," (Set (Var "K")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Set  "(" (Set (Var "H"))  ($#k14_group_2 :::"*"::: )  (Set (Var "x")) ")" )  ($#k11_group_2 :::"*"::: )  (Set (Var "K")))) "iff" (Bool  "ex" (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "x")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "h")))) & (Bool (Set (Var "g"))  ($#r1_struct_0 :::"in"::: )  (Set (Var "H"))) & (Bool (Set (Var "h"))  ($#r1_struct_0 :::"in"::: )  (Set (Var "K")))  ")" ))  ")" )))) ; 
 
theorem :: GROUP_8:18 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "H")) "," (Set (Var "K")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "H"))  ($#k14_group_2 :::"*"::: )  (Set (Var "x")) ")" )  ($#k11_group_2 :::"*"::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "H"))  ($#k14_group_2 :::"*"::: )  (Set (Var "y")) ")" )  ($#k11_group_2 :::"*"::: )  (Set (Var "K")))) "or" (Bool  "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Set  "(" (Set (Var "H"))  ($#k14_group_2 :::"*"::: )  (Set (Var "x")) ")" )  ($#k11_group_2 :::"*"::: )  (Set (Var "K")))) "or"  "not" (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Set  "(" (Set (Var "H"))  ($#k14_group_2 :::"*"::: )  (Set (Var "y")) ")" )  ($#k11_group_2 :::"*"::: )  (Set (Var "K"))))  ")" ))  ")" )))) ; 
 










registrationlet "G" be   ($#l3_algstr_0 :::"Group":::); let "A" be    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); 
cluster (Set   ($#k15_group_2 :::"Left_Cosets"::: )  "A") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; notationlet "G" be   ($#l3_algstr_0 :::"Group":::); let "H" be    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); synonym  :::"index":::  "(" "G" "," "H" ")"  for  :::"index"::: "H"; end; 
theorem :: GROUP_8:19 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "D")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "D"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k10_group_2 :::"/\"::: )  (Set (Var "B")))) & (Bool (Set (Var "G")) "is"   ($#v8_struct_0 :::"finite"::: )  )) "holds"  (Bool (Set   ($#k18_group_2 :::"index"::: )   "(" (Set (Var "G")) "," (Set (Var "B")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k18_group_2 :::"index"::: )   "(" (Set (Var "A")) "," (Set (Var "D")) ")" ))))) ; 
 
theorem :: GROUP_8:20 (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   ($#k18_group_2 :::"index"::: )   "(" (Set (Var "G")) "," (Set (Var "H")) ")" )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: GROUP_8:21 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v8_struct_0 :::"finite"::: )  )) "holds"  (Bool  "for" (Set (Var "C")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "C"))  (Bool  "for" (Set (Var "D")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "D"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k10_group_2 :::"/\"::: )  (Set (Var "B"))))) "holds"  (Bool  "for" (Set (Var "E")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "B"))  "st" (Bool (Bool (Set (Var "E"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k10_group_2 :::"/\"::: )  (Set (Var "B"))))) "holds"  (Bool  "for" (Set (Var "F")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k10_group_2 :::"/\"::: )  (Set (Var "B")))) & (Bool (Set   ($#k18_group_2 :::"index"::: )   "(" (Set (Var "C")) "," (Set (Var "A")) ")" ) "," (Set   ($#k18_group_2 :::"index"::: )   "(" (Set (Var "C")) "," (Set (Var "B")) ")" )  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k18_group_2 :::"index"::: )   "(" (Set (Var "C")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k18_group_2 :::"index"::: )   "(" (Set (Var "A")) "," (Set (Var "D")) ")" )) & (Bool (Set   ($#k18_group_2 :::"index"::: )   "(" (Set (Var "C")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k18_group_2 :::"index"::: )   "(" (Set (Var "B")) "," (Set (Var "E")) ")" ))  ")" ))))))) ; 
 
theorem :: GROUP_8:22 (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"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_struct_0 :::"in"::: )  (Set (Var "H")))) "holds"  (Bool  "for" (Set (Var "j")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set (Var "j")))  ($#r1_struct_0 :::"in"::: )  (Set (Var "H"))))))) ; 
 
theorem :: GROUP_8:23 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set (Var "G"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_group_2 :::"(1)."::: )  (Set (Var "G"))))) "holds"  (Bool  "ex" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "G")))))) ; 
 
theorem :: GROUP_8:24 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_group_4 :::"gr"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )))) "holds"  (Bool  "for" (Set (Var "H")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "H"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_group_2 :::"(1)."::: )  (Set (Var "G"))))) "holds"  (Bool  "ex" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set (Var "k")))  ($#r1_struct_0 :::"in"::: )  (Set (Var "H")))  ")" ))))) ; 
 
theorem :: GROUP_8:25 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#v1_gr_cy_1 :::"cyclic"::: )    ($#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 (Var "H")) "is"   ($#v1_gr_cy_1 :::"cyclic"::: )    ($#l3_algstr_0 :::"Group":::)))) ;