:: CAYLEY  semantic presentation begin  









registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_partit_2 :::"{}"::: )   "(" "X" "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ->   ($#v2_funct_2 :::"onto"::: )   ; 
end; registration
cluster   ($#v3_matrix_2 :::"permutational"::: )    ->   ($#v4_funct_1 :::"functional"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"permutations"::: "X" ->    ($#m1_hidden :::"set"::: )   equals :: CAYLEY:def 1  "{"  (Set (Var "f")) where f "is"   ($#m1_subset_1 :::"Permutation":::) "of" "X" : (Bool verum)  "}"  ; end; 





:: deftheorem    defines :::"permutations"::: CAYLEY:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_cayley :::"permutations"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "f")) where f "is"   ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")) : (Bool verum)  "}"  )); 
 
theorem :: CAYLEY:1 (Bool  "for" (Set (Var "X")) "," (Set (Var "f")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_cayley :::"permutations"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")))) ; 
 
theorem :: CAYLEY:2 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_cayley :::"permutations"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set (Var "X")) ")" ))) ; 
 
theorem :: CAYLEY:3 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_cayley :::"permutations"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k12_matrix_2 :::"Permutations"::: )  (Set (Var "n"))))) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_cayley :::"permutations"::: )  "X") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_funct_1 :::"functional"::: )   ; 
end; registrationlet "X" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_cayley :::"permutations"::: )  "X") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: CAYLEY:4 (Bool (Set   ($#k1_cayley :::"permutations"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"SymGroup"::: "X" ->   ($#v15_algstr_0 :::"strict"::: )     ($#v1_monoid_0 :::"constituted-Functions"::: )     ($#l3_algstr_0 :::"multMagma"::: )   means :: CAYLEY:def 2 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k1_cayley :::"permutations"::: )  "X")) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" it "holds"  (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "x"))))  ")" )  ")" ); end; 





:: deftheorem    defines :::"SymGroup"::: CAYLEY:def 2 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#v1_monoid_0 :::"constituted-Functions"::: )     ($#l3_algstr_0 :::"multMagma"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_cayley :::"SymGroup"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_cayley :::"permutations"::: )  (Set (Var "X")))) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b2")) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "x"))))  ")" )  ")" )  ")" ))); 
 
theorem :: CAYLEY:5 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_cayley :::"SymGroup"::: )  (Set (Var "X")) ")" ) "holds"  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X"))))) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_cayley :::"SymGroup"::: )  "X") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v15_algstr_0 :::"strict"::: )     ($#v2_group_1 :::"Group-like"::: )     ($#v3_group_1 :::"associative"::: )     ($#v1_monoid_0 :::"constituted-Functions"::: )   ; 
end; 
theorem :: CAYLEY:6 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_group_1 :::"1_"::: )  (Set  "("  ($#k2_cayley :::"SymGroup"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set (Var "X"))))) ; 
 
theorem :: CAYLEY:7 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_cayley :::"SymGroup"::: )  (Set (Var "X")) ")" ) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_group_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k2_funct_1 :::"""::: )  )))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k13_matrix_2 :::"Group_of_Perm"::: )  "n") ->   ($#v1_monoid_0 :::"constituted-Functions"::: )   ; 
end; 
theorem :: CAYLEY:8 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k2_cayley :::"SymGroup"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k13_matrix_2 :::"Group_of_Perm"::: )  (Set (Var "n"))))) ; 
 registrationlet "X" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_cayley :::"SymGroup"::: )  "X") ->   ($#v8_struct_0 :::"finite"::: )     ($#v15_algstr_0 :::"strict"::: )     ($#v1_monoid_0 :::"constituted-Functions"::: )   ; 
end; 
theorem :: CAYLEY:9 (Bool (Set   ($#k2_cayley :::"SymGroup"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k7_algstr_0 :::"Trivial-multMagma"::: )  )) ; 
 registration
cluster (Set   ($#k2_cayley :::"SymGroup"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) )) ->   ($#v7_struct_0 :::"trivial"::: )     ($#v15_algstr_0 :::"strict"::: )     ($#v1_monoid_0 :::"constituted-Functions"::: )   ; 
end; definitionlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; let "p" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); assume that  
(Bool  "("  (Bool (Set (Const "X"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Const "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )
 and  
(Bool (Set (Const "p")) "is"   ($#v3_funct_2 :::"bijective"::: )  )
 ; func  :::"SymGroupsIso"::: "p" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_cayley :::"SymGroup"::: )  "X" ")" ) "," (Set  "("  ($#k2_cayley :::"SymGroup"::: )  "Y" ")" ) means :: CAYLEY:def 3 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_cayley :::"SymGroup"::: )  "X" ")" ) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "p"  ($#k3_relat_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "(" "p"  ($#k2_funct_1 :::"""::: )  ")" )))); end; 








:: deftheorem    defines :::"SymGroupsIso"::: CAYLEY:def 3 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "p")) "is"   ($#v3_funct_2 :::"bijective"::: )  )) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_cayley :::"SymGroup"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k2_cayley :::"SymGroup"::: )  (Set (Var "Y")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_cayley :::"SymGroupsIso"::: )  (Set (Var "p")))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_cayley :::"SymGroup"::: )  (Set (Var "X")) ")" ) "holds"  (Bool (Set (Set (Var "b4"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k2_funct_1 :::"""::: )  ")" ))))  ")" )))); 
 
theorem :: CAYLEY:10 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v3_funct_2 :::"bijective"::: )  )) "holds"  (Bool (Set   ($#k3_cayley :::"SymGroupsIso"::: )  (Set (Var "p"))) "is"   ($#v1_group_6 :::"multiplicative"::: )  ))) ; 
 
theorem :: CAYLEY:11 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v3_funct_2 :::"bijective"::: )  )) "holds"  (Bool (Set   ($#k3_cayley :::"SymGroupsIso"::: )  (Set (Var "p"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ))) ; 
 
theorem :: CAYLEY:12 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v3_funct_2 :::"bijective"::: )  )) "holds"  (Bool (Set   ($#k3_cayley :::"SymGroupsIso"::: )  (Set (Var "p"))) "is"   ($#v2_funct_2 :::"onto"::: )  ))) ; 
 
theorem :: CAYLEY:13 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "," (Set (Var "Y"))  ($#r2_tarski :::"are_equipotent"::: )  )) "holds"  (Bool (Set   ($#k2_cayley :::"SymGroup"::: )  (Set (Var "X"))) "," (Set   ($#k2_cayley :::"SymGroup"::: )  (Set (Var "Y")))  ($#r2_group_6 :::"are_isomorphic"::: )  )) ; 
 definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); func  :::"CayleyIso"::: "G" ->   ($#m1_subset_1 :::"Function":::) "of" "G" "," (Set  "("  ($#k2_cayley :::"SymGroup"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") ")" ) means :: CAYLEY:def 4 (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Element":::) "of" "G" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topgrp_1 :::"*"::: )  (Set (Var "g"))))); end; 





:: deftheorem    defines :::"CayleyIso"::: CAYLEY:def 4 :  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set  "("  ($#k2_cayley :::"SymGroup"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_cayley :::"CayleyIso"::: )  (Set (Var "G")))) "iff" (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topgrp_1 :::"*"::: )  (Set (Var "g")))))  ")" ))); 
 registrationlet "G" be   ($#l3_algstr_0 :::"Group":::); 
cluster (Set   ($#k4_cayley :::"CayleyIso"::: )  "G") ->   ($#v1_group_6 :::"multiplicative"::: )   ; 
end; registrationlet "G" be   ($#l3_algstr_0 :::"Group":::); 
cluster (Set   ($#k4_cayley :::"CayleyIso"::: )  "G") ->   ($#v2_funct_1 :::"one-to-one"::: )   ; 
end; 
theorem :: CAYLEY:14 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set (Var "G")) "," (Set   ($#k10_group_6 :::"Image"::: )  (Set  "("  ($#k4_cayley :::"CayleyIso"::: )  (Set (Var "G")) ")" ))  ($#r1_group_6 :::"are_isomorphic"::: )  )) ;