:: GR_CY_1  semantic presentation begin  
































registrationlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k6_card_1 :::"Segm"::: )  "n") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionredefine func  :::"addint":::  means :: GR_CY_1:def 1 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "i1")) "," (Set (Var "i2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k33_binop_2 :::"addreal"::: ) )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "i1")) "," (Set (Var "i2")) ")" ))); end; 




:: deftheorem    defines :::"addint"::: GR_CY_1:def 1 :  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k4_numbers :::"INT"::: ) ) "," (Set  ($#k4_numbers :::"INT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k4_numbers :::"INT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k44_binop_2 :::"addint"::: )  )) "iff" (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) "holds"  (Bool (Set (Set (Var "b1"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "i1")) "," (Set (Var "i2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k33_binop_2 :::"addreal"::: ) )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "i1")) "," (Set (Var "i2")) ")" )))  ")" )); 
 
theorem :: GR_CY_1:1 (Bool  "for" (Set (Var "i1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  )  "st" (Bool (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "i1"))  ($#r3_binop_1 :::"is_a_unity_wrt"::: )  (Set   ($#k44_binop_2 :::"addint"::: )  ))) ; 
 
theorem :: GR_CY_1:2 (Bool  "for" (Set (Var "I")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) "holds"  (Bool (Set   ($#k16_rvsum_1 :::"Sum"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k44_binop_2 :::"addint"::: ) )  ($#k1_finsop_1 :::"$$"::: )  (Set (Var "I"))))) ; 
 definitionlet "I" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ); :: original: :::"Sum"::: redefine func  :::"Sum"::: "I" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) equals :: GR_CY_1:def 2 (Set (Set  ($#k44_binop_2 :::"addint"::: ) )  ($#k1_finsop_1 :::"$$"::: )  "I"); end; 





:: deftheorem    defines :::"Sum"::: GR_CY_1:def 2 :  (Bool  "for" (Set (Var "I")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) "holds"  (Bool (Set   ($#k1_gr_cy_1 :::"Sum"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k44_binop_2 :::"addint"::: ) )  ($#k1_finsop_1 :::"$$"::: )  (Set (Var "I"))))); 
 
theorem :: GR_CY_1:3 (Bool (Set   ($#k1_gr_cy_1 :::"Sum"::: )  (Set  "("  ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k4_numbers :::"INT"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; 
 
theorem :: GR_CY_1:4 (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 "I")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) "holds"  (Bool (Set   ($#k3_group_4 :::"Product"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "I")) ")" )  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "a")) ")" )  ($#k4_group_4 :::"|^"::: )  (Set (Var "I")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set  "("  ($#k1_gr_cy_1 :::"Sum"::: )  (Set (Var "I")) ")" )))))) ; 
 
theorem :: GR_CY_1:5 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "b"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k5_group_4 :::"gr"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))) "iff" (Bool  "ex" (Set (Var "j1")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set (Var "j1")))))  ")" ))) ; 
 
theorem :: GR_CY_1:6 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  "holds" (Bool (Bool  "not" (Set (Var "a")) "is"   ($#v4_group_1 :::"being_of_order_0"::: )  )))) ; 
 
theorem :: GR_CY_1:7 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k6_group_1 :::"ord"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_group_1 :::"card"::: )  (Set  "("  ($#k5_group_4 :::"gr"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) ")" ))))) ; 
 
theorem :: GR_CY_1:8 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k6_group_1 :::"ord"::: )  (Set (Var "a")))  ($#r1_nat_d :::"divides"::: )  (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "G")))))) ; 
 
theorem :: GR_CY_1:9 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set  "("  ($#k7_group_1 :::"card"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "G")))))) ; 
 
theorem :: GR_CY_1:10 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set (Var "n")) ")" )  ($#k2_group_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set  "(" (Set  "("  ($#k7_group_1 :::"card"::: )  (Set (Var "G")) ")" )  ($#k21_binop_2 :::"-"::: )  (Set  "(" (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set  "("  ($#k7_group_1 :::"card"::: )  (Set (Var "G")) ")" ) ")" ) ")" )))))) ; 
 registrationlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_group_1 :::"associative"::: )     ($#l3_algstr_0 :::"multMagma"::: )  ; 
cluster (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "," (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" "G") "#)" ) ->   ($#v3_group_1 :::"associative"::: )   ; 
end; registrationlet "G" be   ($#l3_algstr_0 :::"Group":::); 
cluster (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "," (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" "G") "#)" ) ->   ($#v2_group_1 :::"Group-like"::: )   ; 
end; 
theorem :: GR_CY_1:11 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )     ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (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")))))) ; 
 
theorem :: GR_CY_1:12 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )     ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) & (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  )) "holds"  (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_group_2 :::"="::: )  (Set   ($#k6_group_2 :::"(1)."::: )  (Set (Var "G")))) "or" (Bool (Set (Var "H"))  ($#r1_hidden :::"="::: )  (Set (Var "G")))  ")" )))) ; 
 definitionfunc  :::"INT.Group":::  ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v15_algstr_0 :::"strict"::: )     ($#l3_algstr_0 :::"multMagma"::: )   equals :: GR_CY_1:def 3 (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  ($#k4_numbers :::"INT"::: ) ) "," (Set  ($#k44_binop_2 :::"addint"::: ) ) "#)" ); end; 




:: deftheorem    defines :::"INT.Group"::: GR_CY_1:def 3 :  (Bool (Set   ($#k2_gr_cy_1 :::"INT.Group"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  ($#k4_numbers :::"INT"::: ) ) "," (Set  ($#k44_binop_2 :::"addint"::: ) ) "#)" )); 
 registration
cluster (Set   ($#k2_gr_cy_1 :::"INT.Group"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v15_algstr_0 :::"strict"::: )     ($#v2_group_1 :::"Group-like"::: )     ($#v3_group_1 :::"associative"::: )   ; 
end; registration
cluster (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k2_gr_cy_1 :::"INT.Group"::: ) )) ->   ($#v5_membered :::"integer-membered"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k2_gr_cy_1 :::"INT.Group"::: ) ); 
identify ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k6_card_1 :::"Segm"::: )  "n") ->   ($#v6_membered :::"natural-membered"::: )   ; 
end; definitionlet "n" be   ($#m1_hidden :::"Nat":::); assume 
(Bool (Set (Const "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))
 ; func  :::"addint"::: "n" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k7_card_1 :::"Segm"::: )  "n" ")" ) means :: GR_CY_1:def 4 (Bool  "for" (Set (Var "k")) "," (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_card_1 :::"Segm"::: )  "n") "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "k")) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Set (Var "l")) ")" )  ($#k4_nat_d :::"mod"::: )  "n"))); end; 






:: deftheorem    defines :::"addint"::: GR_CY_1:def 4 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k7_card_1 :::"Segm"::: )  (Set (Var "n")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_gr_cy_1 :::"addint"::: )  (Set (Var "n")))) "iff" (Bool  "for" (Set (Var "k")) "," (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_card_1 :::"Segm"::: )  (Set (Var "n"))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "k")) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Set (Var "l")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))))  ")" ))); 
 definitionlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::); func  :::"INT.Group"::: "n" ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v15_algstr_0 :::"strict"::: )     ($#l3_algstr_0 :::"multMagma"::: )   equals :: GR_CY_1:def 5 (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "("  ($#k7_card_1 :::"Segm"::: )  "n" ")" ) "," (Set  "("  ($#k3_gr_cy_1 :::"addint"::: )  "n" ")" ) "#)" ); end; 





:: deftheorem    defines :::"INT.Group"::: GR_CY_1:def 5 :  (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k4_gr_cy_1 :::"INT.Group"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "("  ($#k7_card_1 :::"Segm"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k3_gr_cy_1 :::"addint"::: )  (Set (Var "n")) ")" ) "#)" ))); 
 registrationlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k4_gr_cy_1 :::"INT.Group"::: )  "n") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"finite"::: )     ($#v15_algstr_0 :::"strict"::: )     ($#v2_group_1 :::"Group-like"::: )     ($#v3_group_1 :::"associative"::: )   ; 
end; 
theorem :: GR_CY_1:13 (Bool (Set   ($#k1_group_1 :::"1_"::: )  (Set  ($#k2_gr_cy_1 :::"INT.Group"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; 
 
theorem :: GR_CY_1:14 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_group_1 :::"1_"::: )  (Set  "("  ($#k4_gr_cy_1 :::"INT.Group"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 definitionlet "h" be   ($#m1_hidden :::"Integer":::); func  :::"@'"::: "h" ->   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k2_gr_cy_1 :::"INT.Group"::: ) ) equals :: GR_CY_1:def 6 "h"; end; 





:: deftheorem    defines :::"@'"::: GR_CY_1:def 6 :  (Bool  "for" (Set (Var "h")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k5_gr_cy_1 :::"@'"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set (Var "h")))); 
 
theorem :: GR_CY_1:15 (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k2_gr_cy_1 :::"INT.Group"::: ) ) "holds"  (Bool (Set (Set (Var "h"))  ($#k2_group_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k19_binop_2 :::"-"::: )  (Set (Var "h"))))) ; 
 



theorem :: GR_CY_1:16 (Bool  "for" (Set (Var "j1")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Var "j1"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_gr_cy_1 :::"@'"::: )  (Num 1) ")" )  ($#k5_group_1 :::"|^"::: )  (Set (Var "j1"))))) ; 
 definitionlet "IT" be   ($#l3_algstr_0 :::"Group":::); attr "IT" is  :::"cyclic":::  means :: GR_CY_1:def 7 (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "IT") "," (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" "IT") "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_group_4 :::"gr"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )))); end; 




:: deftheorem    defines :::"cyclic"::: GR_CY_1:def 7 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l3_algstr_0 :::"Group":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_gr_cy_1 :::"cyclic"::: )  ) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "IT"))) "," (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "IT"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_group_4 :::"gr"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))))  ")" )); 
 registration
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"::: )     ($#v1_gr_cy_1 :::"cyclic"::: )    for    ($#l3_algstr_0 :::"multMagma"::: )  ; 
end; registrationlet "G" be   ($#l3_algstr_0 :::"Group":::); 
cluster (Set   ($#k6_group_2 :::"(1)."::: )  "G") ->   ($#v1_gr_cy_1 :::"cyclic"::: )   ; 
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"::: )     ($#v1_gr_cy_1 :::"cyclic"::: )    for    ($#l3_algstr_0 :::"multMagma"::: )  ; 
end; 
theorem :: GR_CY_1:17 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::) "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v1_gr_cy_1 :::"cyclic"::: )    ($#l3_algstr_0 :::"Group":::)) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st"  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool  "ex" (Set (Var "j1")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set (Var "j1")))))))  ")" )) ; 
 
theorem :: GR_CY_1:18 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::) "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v1_gr_cy_1 :::"cyclic"::: )  ) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st"  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_group_1 :::"|^"::: )  (Set (Var "n")))))))  ")" )) ; 
 
theorem :: GR_CY_1:19 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::) "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v1_gr_cy_1 :::"cyclic"::: )  ) "iff" (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   ($#k7_group_1 :::"card"::: )  (Set (Var "G")))))  ")" )) ; 
 
theorem :: GR_CY_1:20 (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 (Var "G")) "is"   ($#v1_gr_cy_1 :::"cyclic"::: )  )) "holds"  (Bool (Set (Var "H")) "is"   ($#v1_gr_cy_1 :::"cyclic"::: )  ))) ; 
 
theorem :: GR_CY_1:21 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )     ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "G"))) "is"   ($#v1_int_2 :::"prime"::: )  )) "holds"  (Bool (Set (Var "G")) "is"   ($#v1_gr_cy_1 :::"cyclic"::: )    ($#l3_algstr_0 :::"Group":::))) ; 
 
theorem :: GR_CY_1:22 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k4_gr_cy_1 :::"INT.Group"::: )  (Set (Var "n")) ")" ) "st"  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k4_gr_cy_1 :::"INT.Group"::: )  (Set (Var "n")) ")" ) (Bool  "ex" (Set (Var "j1")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k5_group_1 :::"|^"::: )  (Set (Var "j1")))))))) ; 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_group_1 :::"Group-like"::: )     ($#v3_group_1 :::"associative"::: )     ($#v1_gr_cy_1 :::"cyclic"::: )    ->   ($#v5_group_1 :::"commutative"::: )    for    ($#l3_algstr_0 :::"multMagma"::: )  ; 
end; 
theorem :: GR_CY_1:23 (Bool (Set   ($#k2_gr_cy_1 :::"INT.Group"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k5_group_4 :::"gr"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k5_gr_cy_1 :::"@'"::: )  (Num 1) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ; 
 registration
cluster (Set   ($#k2_gr_cy_1 :::"INT.Group"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v15_algstr_0 :::"strict"::: )     ($#v1_gr_cy_1 :::"cyclic"::: )   ; 
end; registrationlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k4_gr_cy_1 :::"INT.Group"::: )  "n") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v15_algstr_0 :::"strict"::: )     ($#v1_gr_cy_1 :::"cyclic"::: )   ; 
end;