:: GROUP_10  semantic presentation begin  notationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )  ; let "E" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_subset_1 :::"Action":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "S"))) "," (Set (Const "E")); let "s" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); synonym "A" :::"^"::: "s" for "S" :::"."::: "E"; end; definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )  ; let "E" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_subset_1 :::"Action":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "S"))) "," (Set (Const "E")); let "s" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); :: original: :::"^"::: redefine func "A" :::"^"::: "s" ->   ($#m1_subset_1 :::"Function":::) "of" "E" "," "E"; end; definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )  ; let "E" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_subset_1 :::"Action":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "S"))) "," (Set (Const "E")); attr "A" is  :::"being_left_operation":::  means :: GROUP_10:def 1 (Bool  "("  (Bool (Set "A"  ($#k1_group_10 :::"^"::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  "S" ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  "E")) & (Bool  "("   "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Element":::) "of" "S" "holds"  (Bool (Set "A"  ($#k1_group_10 :::"^"::: )  (Set  "(" (Set (Var "s1"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "s2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" "A"  ($#k1_group_10 :::"^"::: )  (Set (Var "s1")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" "A"  ($#k1_group_10 :::"^"::: )  (Set (Var "s2")) ")" )))  ")" )  ")" ); end; 






:: deftheorem    defines :::"being_left_operation"::: GROUP_10:def 1 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "E")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Action":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set (Var "E")) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v1_group_10 :::"being_left_operation"::: )  ) "iff" (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k1_group_10 :::"^"::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Var "S")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set (Var "E")))) & (Bool  "("   "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set (Var "A"))  ($#k1_group_10 :::"^"::: )  (Set  "(" (Set (Var "s1"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "s2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k1_group_10 :::"^"::: )  (Set (Var "s1")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k1_group_10 :::"^"::: )  (Set (Var "s2")) ")" )))  ")" )  ")" )  ")" )))); 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )  ; let "E" be    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" "E" "," "E" ")" )  ($#v5_relat_1 :::"-valued"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_funct_1 :::"Function-like"::: )     ($#v1_partfun1 :::"total"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v1_group_10 :::"being_left_operation"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," (Set  "("  ($#k1_funct_2 :::"Funcs"::: )   "(" "E" "," "E" ")"  ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )  ; let "E" be    ($#m1_hidden :::"set"::: )  ; mode LeftOperation of "S" "," "E" is   ($#v1_group_10 :::"being_left_operation"::: )    ($#m1_subset_1 :::"Action":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," "E"; end; scheme  :: GROUP_10:sch 1 ExLeftOperation{ F1() ->    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_group_1 :::"Group-like"::: )     ($#l3_algstr_0 :::"multMagma"::: )  , F3(  ($#m1_subset_1 :::"Element":::) "of" (Set F2 "("  ")" )) ->   ($#m1_subset_1 :::"Function":::) "of" (Set F1 "("  ")" ) "," (Set F1 "("  ")" ) } : 
(Bool  "ex" (Set (Var "T")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set F2 "("  ")" ) "," (Set F1 "("  ")" ) "st"  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set F2 "("  ")" ) "holds"  (Bool (Set (Set (Var "T"))  ($#k3_funct_2 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "s")) ")" ))))
 provided
(Bool (Set F3 "(" (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set F2 "("  ")" ) ")" ) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set F1 "("  ")" )))
 and  
(Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set F2 "("  ")" ) "holds"  (Bool (Set F3 "(" (Set  "(" (Set (Var "s1"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "s2")) ")" ) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Set F3 "(" (Set (Var "s1")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set F3 "(" (Set (Var "s2")) ")" ))))
 proof 


end; registrationlet "E" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_group_1 :::"Group-like"::: )     ($#l3_algstr_0 :::"multMagma"::: )  ; let "s" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "LO" be   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Const "S")) "," (Set (Const "E")); 
cluster (Set   ($#k1_funct_1 :::"^"::: )  ) ->   ($#v2_funct_1 :::"one-to-one"::: )    for  ($#m1_subset_1 :::"Function":::) "of" "E" "," "E"; 
end; notationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_algstr_0 :::"multMagma"::: )  ; let "s" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); synonym  :::"the_left_translation_of"::: "s" for "s" :::"*"::: ; end; definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_group_1 :::"Group-like"::: )     ($#v3_group_1 :::"associative"::: )     ($#l3_algstr_0 :::"multMagma"::: )  ; func  :::"the_left_operation_of"::: "S" ->   ($#m1_subset_1 :::"LeftOperation":::) "of" "S" "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") means :: GROUP_10:def 2 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" "S" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_topgrp_1 :::"the_left_translation_of"::: )  (Set (Var "s"))))); end; 





:: deftheorem    defines :::"the_left_operation_of"::: GROUP_10:def 2 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_group_1 :::"Group-like"::: )     ($#v3_group_1 :::"associative"::: )     ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "S")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_group_10 :::"the_left_operation_of"::: )  (Set (Var "S")))) "iff" (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_topgrp_1 :::"the_left_translation_of"::: )  (Set (Var "s")))))  ")" ))); 
 definitionlet "E", "n" be    ($#m1_hidden :::"set"::: )  ; func  :::"the_subsets_of_card":::  "(" "n" "," "E" ")"  ->   ($#m1_subset_1 :::"Subset-Family":::) "of" "E" equals :: GROUP_10:def 3  "{"  (Set (Var "X")) where X "is"   ($#m1_subset_1 :::"Subset":::) "of" "E" : (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  "n")  "}"  ; end; 






:: deftheorem    defines :::"the_subsets_of_card"::: GROUP_10:def 3 :  (Bool  "for" (Set (Var "E")) "," (Set (Var "n")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "n")) "," (Set (Var "E")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "X")) where X "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) : (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  "}"  )); 
 registrationlet "E" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; let "n" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" "n" "," "E" ")" ) ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: GROUP_10:1 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "n")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "E"))))) "holds"  (Bool  "not" (Bool (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "n")) "," (Set (Var "E")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  )))) ; 
 
theorem :: GROUP_10:2 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x2")))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_card_fin :::"Choose"::: )   "(" (Set (Var "E")) "," (Set (Var "k")) "," (Set (Var "x1")) "," (Set (Var "x2")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "k")) "," (Set (Var "E")) ")"  ")" )))))) ; 
 definitionlet "E" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "n" be   ($#m1_hidden :::"Nat":::); let "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_group_1 :::"Group-like"::: )     ($#l3_algstr_0 :::"multMagma"::: )  ; let "s" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "LO" be   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Const "S")) "," (Set (Const "E")); assume 
(Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Const "n")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Const "E"))))
 ; func  :::"the_extension_of_left_translation_of":::  "(" "n" "," "s" "," "LO" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" "n" "," "E" ")"  ")" ) "," (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" "n" "," "E" ")"  ")" ) means :: GROUP_10:def 4 (Bool  "for" (Set (Var "X")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" "n" "," "E" ")" ) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "LO"  ($#k1_group_10 :::"^"::: )  "s" ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "X"))))); end; 










:: deftheorem    defines :::"the_extension_of_left_translation_of"::: GROUP_10:def 4 :  (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_group_1 :::"Group-like"::: )     ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "LO")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "S")) "," (Set (Var "E"))  "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "n")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "E"))))) "holds"  (Bool  "for" (Set (Var "b6")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "n")) "," (Set (Var "E")) ")"  ")" ) "," (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "n")) "," (Set (Var "E")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b6"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_group_10 :::"the_extension_of_left_translation_of"::: )   "(" (Set (Var "n")) "," (Set (Var "s")) "," (Set (Var "LO")) ")" )) "iff" (Bool  "for" (Set (Var "X")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "n")) "," (Set (Var "E")) ")" ) "holds"  (Bool (Set (Set (Var "b6"))  ($#k1_funct_1 :::"."::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "LO"))  ($#k1_group_10 :::"^"::: )  (Set (Var "s")) ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")))))  ")" ))))))); 
 definitionlet "E" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "n" be   ($#m1_hidden :::"Nat":::); let "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_group_1 :::"Group-like"::: )     ($#l3_algstr_0 :::"multMagma"::: )  ; let "LO" be   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Const "S")) "," (Set (Const "E")); assume 
(Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Const "n")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Const "E"))))
 ; func  :::"the_extension_of_left_operation_of":::  "(" "n" "," "LO" ")"  ->   ($#m1_subset_1 :::"LeftOperation":::) "of" "S" "," (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" "n" "," "E" ")"  ")" ) means :: GROUP_10:def 5 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" "S" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_group_10 :::"the_extension_of_left_translation_of"::: )   "(" "n" "," (Set (Var "s")) "," "LO" ")" ))); end; 









:: deftheorem    defines :::"the_extension_of_left_operation_of"::: GROUP_10:def 5 :  (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_group_1 :::"Group-like"::: )     ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "LO")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "S")) "," (Set (Var "E"))  "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "n")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "E"))))) "holds"  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "S")) "," (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "n")) "," (Set (Var "E")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_group_10 :::"the_extension_of_left_operation_of"::: )   "(" (Set (Var "n")) "," (Set (Var "LO")) ")" )) "iff" (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set (Var "b5"))  ($#k3_funct_2 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_group_10 :::"the_extension_of_left_translation_of"::: )   "(" (Set (Var "n")) "," (Set (Var "s")) "," (Set (Var "LO")) ")" )))  ")" )))))); 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_algstr_0 :::"multMagma"::: )  ; let "s" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "Z" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; func  :::"the_left_translation_of":::  "(" "s" "," "Z" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," "Z" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," "Z" ($#k2_zfmisc_1 :::":]"::: ) ) means :: GROUP_10:def 6 (Bool  "for" (Set (Var "z1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," "Z" ($#k2_zfmisc_1 :::":]"::: ) ) (Bool  "ex" (Set (Var "z2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," "Z" ($#k2_zfmisc_1 :::":]"::: ) )(Bool  "ex" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Element":::) "of" "S"(Bool  "ex" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "Z" "st"  (Bool  "("  (Bool (Set (Var "z2"))  ($#r1_hidden :::"="::: )  (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "z1")))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set "s"  ($#k6_algstr_0 :::"*"::: )  (Set (Var "s1")))) & (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "z2"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) ))  ")" ))))); end; 







:: deftheorem    defines :::"the_left_translation_of"::: GROUP_10:def 6 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "Z")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_group_10 :::"the_left_translation_of"::: )   "(" (Set (Var "s")) "," (Set (Var "Z")) ")" )) "iff" (Bool  "for" (Set (Var "z1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool  "ex" (Set (Var "z2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) )(Bool  "ex" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))(Bool  "ex" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "Z")) "st"  (Bool  "("  (Bool (Set (Var "z2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b4"))  ($#k3_funct_2 :::"."::: )  (Set (Var "z1")))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "s1")))) & (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "z2"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) ))  ")" )))))  ")" ))))); 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_group_1 :::"Group-like"::: )     ($#v3_group_1 :::"associative"::: )     ($#l3_algstr_0 :::"multMagma"::: )  ; let "Z" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; func  :::"the_left_operation_of":::  "(" "S" "," "Z" ")"  ->   ($#m1_subset_1 :::"LeftOperation":::) "of" "S" "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," "Z" ($#k2_zfmisc_1 :::":]"::: ) ) means :: GROUP_10:def 7 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" "S" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_group_10 :::"the_left_translation_of"::: )   "(" (Set (Var "s")) "," "Z" ")" ))); end; 






:: deftheorem    defines :::"the_left_operation_of"::: GROUP_10:def 7 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_group_1 :::"Group-like"::: )     ($#v3_group_1 :::"associative"::: )     ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "Z")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "S")) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_group_10 :::"the_left_operation_of"::: )   "(" (Set (Var "S")) "," (Set (Var "Z")) ")" )) "iff" (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_group_10 :::"the_left_translation_of"::: )   "(" (Set (Var "s")) "," (Set (Var "Z")) ")" )))  ")" )))); 
 definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "H", "P" be    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); let "h" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "H")); func  :::"the_left_translation_of":::  "(" "h" "," "P" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_group_2 :::"Left_Cosets"::: )  "P" ")" ) "," (Set  "("  ($#k15_group_2 :::"Left_Cosets"::: )  "P" ")" ) means :: GROUP_10:def 8 (Bool  "for" (Set (Var "P1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k15_group_2 :::"Left_Cosets"::: )  "P") (Bool  "ex" (Set (Var "P2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k15_group_2 :::"Left_Cosets"::: )  "P")(Bool  "ex" (Set (Var "A1")) "," (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "G"(Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Element":::) "of" "G" "st"  (Bool  "("  (Bool (Set (Var "P2"))  ($#r1_hidden :::"="::: )  (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "P1")))) & (Bool (Set (Var "A2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k4_group_2 :::"*"::: )  (Set (Var "A1")))) & (Bool (Set (Var "A1"))  ($#r1_hidden :::"="::: )  (Set (Var "P1"))) & (Bool (Set (Var "A2"))  ($#r1_hidden :::"="::: )  (Set (Var "P2"))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  "h")  ")" ))))); end; 








:: deftheorem    defines :::"the_left_translation_of"::: GROUP_10:def 8 :  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "H")) "," (Set (Var "P")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H"))  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_group_2 :::"Left_Cosets"::: )  (Set (Var "P")) ")" ) "," (Set  "("  ($#k15_group_2 :::"Left_Cosets"::: )  (Set (Var "P")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_group_10 :::"the_left_translation_of"::: )   "(" (Set (Var "h")) "," (Set (Var "P")) ")" )) "iff" (Bool  "for" (Set (Var "P1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k15_group_2 :::"Left_Cosets"::: )  (Set (Var "P"))) (Bool  "ex" (Set (Var "P2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k15_group_2 :::"Left_Cosets"::: )  (Set (Var "P")))(Bool  "ex" (Set (Var "A1")) "," (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G"))(Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "P2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b5"))  ($#k1_funct_1 :::"."::: )  (Set (Var "P1")))) & (Bool (Set (Var "A2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k4_group_2 :::"*"::: )  (Set (Var "A1")))) & (Bool (Set (Var "A1"))  ($#r1_hidden :::"="::: )  (Set (Var "P1"))) & (Bool (Set (Var "A2"))  ($#r1_hidden :::"="::: )  (Set (Var "P2"))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "h")))  ")" )))))  ")" ))))); 
 definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "H", "P" be    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); func  :::"the_left_operation_of":::  "(" "H" "," "P" ")"  ->   ($#m1_subset_1 :::"LeftOperation":::) "of" "H" "," (Set  "("  ($#k15_group_2 :::"Left_Cosets"::: )  "P" ")" ) means :: GROUP_10:def 9 (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Element":::) "of" "H" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_group_10 :::"the_left_translation_of"::: )   "(" (Set (Var "h")) "," "P" ")" ))); end; 







:: deftheorem    defines :::"the_left_operation_of"::: GROUP_10:def 9 :  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "H")) "," (Set (Var "P")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "H")) "," (Set  "("  ($#k15_group_2 :::"Left_Cosets"::: )  (Set (Var "P")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_group_10 :::"the_left_operation_of"::: )   "(" (Set (Var "H")) "," (Set (Var "P")) ")" )) "iff" (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds"  (Bool (Set (Set (Var "b4"))  ($#k3_funct_2 :::"."::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_group_10 :::"the_left_translation_of"::: )   "(" (Set (Var "h")) "," (Set (Var "P")) ")" )))  ")" )))); 
 begin  definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "E" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Const "G")) "," (Set (Const "E")); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "E")); func  :::"the_strict_stabilizer_of":::  "(" "A" "," "T" ")"  ->   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" "G" means :: GROUP_10:def 10 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )   "{"  (Set (Var "g")) where g "is"   ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool (Set (Set  "(" "T"  ($#k1_group_10 :::"^"::: )  (Set (Var "g")) ")" )  ($#k7_relset_1 :::".:"::: )  "A")  ($#r1_hidden :::"="::: )  "A")  "}"  ); end; 








:: deftheorem    defines :::"the_strict_stabilizer_of"::: GROUP_10:def 10 :  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "G")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E"))  (Bool  "for" (Set (Var "b5")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_group_10 :::"the_strict_stabilizer_of"::: )   "(" (Set (Var "A")) "," (Set (Var "T")) ")" )) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b5")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "g")) where g "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool (Set (Set  "(" (Set (Var "T"))  ($#k1_group_10 :::"^"::: )  (Set (Var "g")) ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "A")))  "}"  )  ")" )))))); 
 definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "E" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Const "G")) "," (Set (Const "E")); let "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "E")); func  :::"the_strict_stabilizer_of":::  "(" "x" "," "T" ")"  ->   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" "G" equals :: GROUP_10:def 11 (Set   ($#k10_group_10 :::"the_strict_stabilizer_of"::: )   "(" (Set  ($#k6_domain_1 :::"{"::: ) "x" ($#k6_domain_1 :::"}"::: ) ) "," "T" ")" ); end; 








:: deftheorem    defines :::"the_strict_stabilizer_of"::: GROUP_10:def 11 :  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "G")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) "holds"  (Bool (Set   ($#k11_group_10 :::"the_strict_stabilizer_of"::: )   "(" (Set (Var "x")) "," (Set (Var "T")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k10_group_10 :::"the_strict_stabilizer_of"::: )   "(" (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) "," (Set (Var "T")) ")" )))))); 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )  ; let "E" be    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Const "S")) "," (Set (Const "E")); let "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "E")); pred "x" :::"is_fixed_under"::: "T" means :: GROUP_10:def 12 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" "S" "holds"  (Bool "x"  ($#r1_hidden :::"="::: )  (Set (Set  "(" "T"  ($#k1_group_10 :::"^"::: )  (Set (Var "s")) ")" )  ($#k1_funct_1 :::"."::: )  "x"))); end; 







:: deftheorem    defines :::"is_fixed_under"::: GROUP_10:def 12 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "E")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "S")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_group_10 :::"is_fixed_under"::: )  (Set (Var "T"))) "iff" (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "T"))  ($#k1_group_10 :::"^"::: )  (Set (Var "s")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))))  ")" ))))); 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )  ; let "E" be    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Const "S")) "," (Set (Const "E")); func  :::"the_fixed_points_of"::: "T" ->   ($#m1_subset_1 :::"Subset":::) "of" "E" equals :: GROUP_10:def 13  "{"  (Set (Var "x")) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" "E" : (Bool (Set (Var "x"))  ($#r1_group_10 :::"is_fixed_under"::: )  "T")  "}"   if (Bool (Bool  "not" "E" "is"   ($#v1_xboole_0 :::"empty"::: )  ))  otherwise (Set   ($#k1_subset_1 :::"{}"::: )  "E"); end; 







:: deftheorem    defines :::"the_fixed_points_of"::: GROUP_10:def 13 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "E")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "S")) "," (Set (Var "E")) "holds"   (Bool  "("   "("  (Bool (Bool (Bool  "not" (Set (Var "E")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool (Set   ($#k12_group_10 :::"the_fixed_points_of"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) : (Bool (Set (Var "x"))  ($#r1_group_10 :::"is_fixed_under"::: )  (Set (Var "T")))  "}"  )  ")"  &  "("  (Bool (Bool (Set (Var "E")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) "implies" (Bool (Set   ($#k12_group_10 :::"the_fixed_points_of"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_subset_1 :::"{}"::: )  (Set (Var "E"))))  ")"   ")" )))); 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )  ; let "E" be    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Const "S")) "," (Set (Const "E")); let "x", "y" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "E")); pred "x" "," "y" :::"are_conjugated_under"::: "T" means :: GROUP_10:def 14 (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" "S" "st" (Bool "y"  ($#r1_hidden :::"="::: )  (Set (Set  "(" "T"  ($#k1_group_10 :::"^"::: )  (Set (Var "s")) ")" )  ($#k1_funct_1 :::"."::: )  "x"))); end; 








:: deftheorem    defines :::"are_conjugated_under"::: GROUP_10:def 14 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "E")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "S")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) "holds"   (Bool  "("  (Bool (Set (Var "x")) "," (Set (Var "y"))  ($#r2_group_10 :::"are_conjugated_under"::: )  (Set (Var "T"))) "iff" (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "T"))  ($#k1_group_10 :::"^"::: )  (Set (Var "s")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))))  ")" ))))); 
 
theorem :: GROUP_10:3 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E"))  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "S")) "," (Set (Var "E")) "holds"  (Bool (Set (Var "x")) "," (Set (Var "x"))  ($#r2_group_10 :::"are_conjugated_under"::: )  (Set (Var "T"))))))) ; 
 
theorem :: GROUP_10:4 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E"))  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "G")) "," (Set (Var "E"))  "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y"))  ($#r2_group_10 :::"are_conjugated_under"::: )  (Set (Var "T")))) "holds"  (Bool (Set (Var "y")) "," (Set (Var "x"))  ($#r2_group_10 :::"are_conjugated_under"::: )  (Set (Var "T"))))))) ; 
 
theorem :: GROUP_10:5 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E"))  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "S")) "," (Set (Var "E"))  "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y"))  ($#r2_group_10 :::"are_conjugated_under"::: )  (Set (Var "T"))) & (Bool (Set (Var "y")) "," (Set (Var "z"))  ($#r2_group_10 :::"are_conjugated_under"::: )  (Set (Var "T")))) "holds"  (Bool (Set (Var "x")) "," (Set (Var "z"))  ($#r2_group_10 :::"are_conjugated_under"::: )  (Set (Var "T"))))))) ; 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )  ; let "E" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Const "S")) "," (Set (Const "E")); let "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "E")); func  :::"the_orbit_of":::  "(" "x" "," "T" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" "E" equals :: GROUP_10:def 15  "{"  (Set (Var "y")) where y "is"    ($#m1_subset_1 :::"Element"::: )   "of" "E" : (Bool "x" "," (Set (Var "y"))  ($#r2_group_10 :::"are_conjugated_under"::: )  "T")  "}"  ; end; 








:: deftheorem    defines :::"the_orbit_of"::: GROUP_10:def 15 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "S")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) "holds"  (Bool (Set   ($#k13_group_10 :::"the_orbit_of"::: )   "(" (Set (Var "x")) "," (Set (Var "T")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "y")) where y "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) : (Bool (Set (Var "x")) "," (Set (Var "y"))  ($#r2_group_10 :::"are_conjugated_under"::: )  (Set (Var "T")))  "}"  ))))); 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )  ; let "E" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "E")); let "T" be   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Const "S")) "," (Set (Const "E")); 
cluster (Set   ($#k13_group_10 :::"the_orbit_of"::: )   "(" "x" "," "T" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: GROUP_10:6 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E"))  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "G")) "," (Set (Var "E"))  "holds"  (Bool  "("  (Bool (Set   ($#k13_group_10 :::"the_orbit_of"::: )   "(" (Set (Var "x")) "," (Set (Var "T")) ")" )  ($#r1_subset_1 :::"misses"::: )  (Set   ($#k13_group_10 :::"the_orbit_of"::: )   "(" (Set (Var "y")) "," (Set (Var "T")) ")" )) "or" (Bool (Set   ($#k13_group_10 :::"the_orbit_of"::: )   "(" (Set (Var "x")) "," (Set (Var "T")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k13_group_10 :::"the_orbit_of"::: )   "(" (Set (Var "y")) "," (Set (Var "T")) ")" ))  ")" ))))) ; 
 
theorem :: GROUP_10:7 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_group_1 :::"unital"::: )     ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E"))  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "S")) "," (Set (Var "E"))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_group_10 :::"is_fixed_under"::: )  (Set (Var "T")))) "holds"  (Bool (Set   ($#k13_group_10 :::"the_orbit_of"::: )   "(" (Set (Var "x")) "," (Set (Var "T")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))))) ; 
 
theorem :: GROUP_10:8 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E"))  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "G")) "," (Set (Var "E")) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k13_group_10 :::"the_orbit_of"::: )   "(" (Set (Var "a")) "," (Set (Var "T")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k17_group_2 :::"Index"::: )  (Set  "("  ($#k11_group_10 :::"the_strict_stabilizer_of"::: )   "(" (Set (Var "a")) "," (Set (Var "T")) ")"  ")" ))))))) ; 
 definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "E" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Const "G")) "," (Set (Const "E")); func  :::"the_orbits_of"::: "T" ->    ($#m1_eqrel_1 :::"a_partition"::: )   "of" "E" equals :: GROUP_10:def 16  "{"  (Set (Var "X")) where X "is"   ($#m1_subset_1 :::"Subset":::) "of" "E" : (Bool  "ex" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "E" "st" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k13_group_10 :::"the_orbit_of"::: )   "(" (Set (Var "x")) "," "T" ")" )))  "}"  ; end; 







:: deftheorem    defines :::"the_orbits_of"::: GROUP_10:def 16 :  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "G")) "," (Set (Var "E")) "holds"  (Bool (Set   ($#k14_group_10 :::"the_orbits_of"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "X")) where X "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) : (Bool  "ex" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) "st" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k13_group_10 :::"the_orbit_of"::: )   "(" (Set (Var "x")) "," (Set (Var "T")) ")" )))  "}"  )))); 
 begin  definitionlet "p" be   ($#m1_hidden :::"Nat":::); let "G" be   ($#l3_algstr_0 :::"Group":::); attr "G" is "p" :::"-group":::  means :: GROUP_10:def 17 (Bool  "ex" (Set (Var "r")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set   ($#k7_struct_0 :::"card"::: )  "G")  ($#r1_hidden :::"="::: )  (Set "p"  ($#k1_newton :::"|^"::: )  (Set (Var "r"))))); end; 





:: deftheorem    defines :::"-group"::: GROUP_10:def 17 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::) "holds"   (Bool  "("  (Bool (Set (Var "G")) "is" (Set (Var "p"))  ($#v2_group_10 :::"-group"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set   ($#k7_struct_0 :::"card"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "r")))))  ")" ))); 
 registrationlet "p" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k4_gr_cy_1 :::"INT.Group"::: )  "p") -> "p"  ($#v2_group_10 :::"-group"::: )   ; 
end; registrationlet "p" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::); 
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"::: )     ($#v5_group_1 :::"commutative"::: )     ($#v1_gr_cy_1 :::"cyclic"::: )   "p"  ($#v2_group_10 :::"-group"::: )    for    ($#l3_algstr_0 :::"multMagma"::: )  ; 
end; 
theorem :: GROUP_10:9 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "p")) "being"   ($#v1_int_2 :::"prime"::: )    ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "G")) "," (Set (Var "E"))  "st" (Bool (Bool (Set (Var "G")) "is" (Set (Var "p"))  ($#v2_group_10 :::"-group"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k12_group_10 :::"the_fixed_points_of"::: )  (Set (Var "T")) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "E")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "p")))))))) ; 
 begin  definitionlet "p" be   ($#m1_hidden :::"Nat":::); let "G" be   ($#l3_algstr_0 :::"Group":::); let "P" be    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); pred "P" :::"is_Sylow_p-subgroup_of_prime"::: "p" means :: GROUP_10:def 18 (Bool  "("  (Bool "P" "is" "p"  ($#v2_group_10 :::"-group"::: )  ) & (Bool (Bool  "not" "p"  ($#r1_nat_d :::"divides"::: )  (Set   ($#k18_group_2 :::"index"::: )  "P")))  ")" ); end; 






:: deftheorem    defines :::"is_Sylow_p-subgroup_of_prime"::: GROUP_10:def 18 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "P")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "P"))  ($#r3_group_10 :::"is_Sylow_p-subgroup_of_prime"::: )  (Set (Var "p"))) "iff" (Bool  "("  (Bool (Set (Var "P")) "is" (Set (Var "p"))  ($#v2_group_10 :::"-group"::: )  ) & (Bool (Bool  "not" (Set (Var "p"))  ($#r1_nat_d :::"divides"::: )  (Set   ($#k18_group_2 :::"index"::: )  (Set (Var "P")))))  ")" )  ")" )))); 
 
theorem :: GROUP_10:10 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "p")) "being"   ($#v1_int_2 :::"prime"::: )    ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "P")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "st" (Bool (Set (Var "P"))  ($#r3_group_10 :::"is_Sylow_p-subgroup_of_prime"::: )  (Set (Var "p")))))) ; 
 
theorem :: GROUP_10:11 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "p")) "being"   ($#v1_int_2 :::"prime"::: )    ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_nat_d :::"divides"::: )  (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "G"))))) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set   ($#k6_group_1 :::"ord"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Var "p")))))) ; 
 
theorem :: GROUP_10:12 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "p")) "being"   ($#v1_int_2 :::"prime"::: )    ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool  "("   "for" (Set (Var "H")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "H")) "is" (Set (Var "p"))  ($#v2_group_10 :::"-group"::: )  )) "holds"  (Bool  "ex" (Set (Var "P")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "P"))  ($#r3_group_10 :::"is_Sylow_p-subgroup_of_prime"::: )  (Set (Var "p"))) & (Bool (Set (Var "H")) "is"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "P")))  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "P1"))  ($#r3_group_10 :::"is_Sylow_p-subgroup_of_prime"::: )  (Set (Var "p"))) & (Bool (Set (Var "P2"))  ($#r3_group_10 :::"is_Sylow_p-subgroup_of_prime"::: )  (Set (Var "p")))) "holds"  (Bool (Set (Var "P1")) "," (Set (Var "P2"))  ($#r5_group_3 :::"are_conjugated"::: )  )  ")" )  ")" ))) ; 
 definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "p" be   ($#m1_hidden :::"Nat":::); func  :::"the_sylow_p-subgroups_of_prime":::  "(" "p" "," "G" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_group_3 :::"Subgroups"::: )  "G" ")" ) equals :: GROUP_10:def 19  "{"  (Set (Var "H")) where H "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_group_3 :::"Subgroups"::: )  "G") : (Bool  "ex" (Set (Var "P")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" "G" "st"  (Bool  "("  (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Var "H"))) & (Bool (Set (Var "P"))  ($#r3_group_10 :::"is_Sylow_p-subgroup_of_prime"::: )  "p")  ")" ))  "}"  ; end; 






:: deftheorem    defines :::"the_sylow_p-subgroups_of_prime"::: GROUP_10:def 19 :  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k15_group_10 :::"the_sylow_p-subgroups_of_prime"::: )   "(" (Set (Var "p")) "," (Set (Var "G")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "H")) where H "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_group_3 :::"Subgroups"::: )  (Set (Var "G"))) : (Bool  "ex" (Set (Var "P")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Var "H"))) & (Bool (Set (Var "P"))  ($#r3_group_10 :::"is_Sylow_p-subgroup_of_prime"::: )  (Set (Var "p")))  ")" ))  "}"  ))); 
 registrationlet "G" be   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::); let "p" be   ($#v1_int_2 :::"prime"::: )    ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k15_group_10 :::"the_sylow_p-subgroups_of_prime"::: )   "(" "p" "," "G" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )   ; 
end; definitionlet "G" be   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::); let "p" be   ($#v1_int_2 :::"prime"::: )    ($#m1_hidden :::"Nat":::); let "H" be    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); let "h" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "H")); func  :::"the_left_translation_of":::  "(" "h" "," "p" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_group_10 :::"the_sylow_p-subgroups_of_prime"::: )   "(" "p" "," "G" ")"  ")" ) "," (Set  "("  ($#k15_group_10 :::"the_sylow_p-subgroups_of_prime"::: )   "(" "p" "," "G" ")"  ")" ) means :: GROUP_10:def 20 (Bool  "for" (Set (Var "P1")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k15_group_10 :::"the_sylow_p-subgroups_of_prime"::: )   "(" "p" "," "G" ")" ) (Bool  "ex" (Set (Var "P2")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k15_group_10 :::"the_sylow_p-subgroups_of_prime"::: )   "(" "p" "," "G" ")" )(Bool  "ex" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" "G"(Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Element":::) "of" "G" "st"  (Bool  "("  (Bool (Set (Var "P2"))  ($#r1_hidden :::"="::: )  (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "P1")))) & (Bool (Set (Var "P1"))  ($#r1_hidden :::"="::: )  (Set (Var "H1"))) & (Bool (Set (Var "P2"))  ($#r1_hidden :::"="::: )  (Set (Var "H2"))) & (Bool (Set "h"  ($#k2_group_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "H2"))  ($#r1_group_2 :::"="::: )  (Set (Set (Var "H1"))  ($#k6_group_3 :::"|^"::: )  (Set (Var "g"))))  ")" ))))); end; 








:: deftheorem    defines :::"the_left_translation_of"::: GROUP_10:def 20 :  (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "p")) "being"   ($#v1_int_2 :::"prime"::: )    ($#m1_hidden :::"Nat":::)  (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"))  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_group_10 :::"the_sylow_p-subgroups_of_prime"::: )   "(" (Set (Var "p")) "," (Set (Var "G")) ")"  ")" ) "," (Set  "("  ($#k15_group_10 :::"the_sylow_p-subgroups_of_prime"::: )   "(" (Set (Var "p")) "," (Set (Var "G")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k16_group_10 :::"the_left_translation_of"::: )   "(" (Set (Var "h")) "," (Set (Var "p")) ")" )) "iff" (Bool  "for" (Set (Var "P1")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k15_group_10 :::"the_sylow_p-subgroups_of_prime"::: )   "(" (Set (Var "p")) "," (Set (Var "G")) ")" ) (Bool  "ex" (Set (Var "P2")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k15_group_10 :::"the_sylow_p-subgroups_of_prime"::: )   "(" (Set (Var "p")) "," (Set (Var "G")) ")" )(Bool  "ex" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))(Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "P2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b5"))  ($#k3_funct_2 :::"."::: )  (Set (Var "P1")))) & (Bool (Set (Var "P1"))  ($#r1_hidden :::"="::: )  (Set (Var "H1"))) & (Bool (Set (Var "P2"))  ($#r1_hidden :::"="::: )  (Set (Var "H2"))) & (Bool (Set (Set (Var "h"))  ($#k2_group_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "H2"))  ($#r1_group_2 :::"="::: )  (Set (Set (Var "H1"))  ($#k6_group_3 :::"|^"::: )  (Set (Var "g"))))  ")" )))))  ")" )))))); 
 definitionlet "G" be   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::); let "p" be   ($#v1_int_2 :::"prime"::: )    ($#m1_hidden :::"Nat":::); let "H" be    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Const "G")); func  :::"the_left_operation_of":::  "(" "H" "," "p" ")"  ->   ($#m1_subset_1 :::"LeftOperation":::) "of" "H" "," (Set  "("  ($#k15_group_10 :::"the_sylow_p-subgroups_of_prime"::: )   "(" "p" "," "G" ")"  ")" ) means :: GROUP_10:def 21 (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Element":::) "of" "H" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set   ($#k16_group_10 :::"the_left_translation_of"::: )   "(" (Set (Var "h")) "," "p" ")" ))); end; 







:: deftheorem    defines :::"the_left_operation_of"::: GROUP_10:def 21 :  (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "p")) "being"   ($#v1_int_2 :::"prime"::: )    ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "H")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"LeftOperation":::) "of" (Set (Var "H")) "," (Set  "("  ($#k15_group_10 :::"the_sylow_p-subgroups_of_prime"::: )   "(" (Set (Var "p")) "," (Set (Var "G")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k17_group_10 :::"the_left_operation_of"::: )   "(" (Set (Var "H")) "," (Set (Var "p")) ")" )) "iff" (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds"  (Bool (Set (Set (Var "b4"))  ($#k3_funct_2 :::"."::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set   ($#k16_group_10 :::"the_left_translation_of"::: )   "(" (Set (Var "h")) "," (Set (Var "p")) ")" )))  ")" ))))); 
 
theorem :: GROUP_10:13 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "p")) "being"   ($#v1_int_2 :::"prime"::: )    ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k15_group_10 :::"the_sylow_p-subgroups_of_prime"::: )   "(" (Set (Var "p")) "," (Set (Var "G")) ")"  ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k15_group_10 :::"the_sylow_p-subgroups_of_prime"::: )   "(" (Set (Var "p")) "," (Set (Var "G")) ")"  ")" ))  ($#r1_nat_d :::"divides"::: )  (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "G"))))  ")" ))) ; 
 begin  
theorem :: GROUP_10:14 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) where y "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "Y")) : (Bool verum)  "}"  )  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y"))))) ; 
 
theorem :: GROUP_10:15 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "r")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#v1_int_2 :::"prime"::: )    ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "r")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m")))) & (Bool (Bool  "not" (Set (Var "p"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "m"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k6_newton :::"choose"::: )  (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "r")) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "p")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: GROUP_10:16 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set  "("  ($#k4_gr_cy_1 :::"INT.Group"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) ; 
 
theorem :: GROUP_10:17 (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 "g")) "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 (Var "A"))  ($#k5_group_2 :::"*"::: )  (Set (Var "g")) ")" )))))) ;