:: CAYLEY semantic presentation

begin


registration
let X be set ;
cluster {} (X,{}) ->  onto ;
coherence
 {} (X,{}) is onto
proof
thus  rng ({} (X,{})) = {} ; :: according to FUNCT_2:def_3 ::_thesis: verum
end;
end;

registration
cluster permutational  ->  functional for set ;
coherence
 for b1 being set st b1 is permutational holds
b1 is functional
proof
let X be set ; ::_thesis: ( X is permutational implies X is functional )
assume  X is permutational ; ::_thesis: X is functional
then A1: ex n being Nat st
for x being set st x in X holds
x is Permutation of (Seg n) by MATRIX_2:def_7;
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in X or x is set )
thus  ( not x in X or x is set ) by A1; ::_thesis: verum
end;
end;

definition
let X be set ;
func permutations X ->  set  equals :: CAYLEY:def 1
 {  f where f is Permutation of X : verum  }  ;
coherence
  {  f where f is Permutation of X : verum  }  is set ;
end;

:: deftheorem  defines permutations CAYLEY:def_1_:_
 for X being set holds permutations X =  {  f where f is Permutation of X : verum  }  ;

theorem Th1: :: CAYLEY:1
for X, f being set st f in permutations X holds
f is Permutation of X
proof
let X, f be set ; ::_thesis: ( f in permutations X implies f is Permutation of X )
assume  f in permutations X ; ::_thesis: f is Permutation of X
then  ex g being Permutation of X st g = f ;
hence  f is Permutation of X ; ::_thesis: verum
end;

theorem Th2: :: CAYLEY:2
for X being set holds permutations X c= Funcs (X,X)
proof
let X be set ; ::_thesis: permutations X c= Funcs (X,X)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in permutations X or x in Funcs (X,X) )
assume  x in permutations X ; ::_thesis: x in Funcs (X,X)
then  x is Permutation of X by Th1;
hence  x in Funcs (X,X) by FUNCT_2:9; ::_thesis: verum
end;

theorem Th3: :: CAYLEY:3
for n being Nat holds permutations (Seg n) = Permutations n
proof
let n be Nat; ::_thesis: permutations (Seg n) = Permutations n
thus  permutations (Seg n) c= Permutations n :: according to XBOOLE_0:def_10 ::_thesis: Permutations n c= permutations (Seg n)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in permutations (Seg n) or x in Permutations n )
assume  x in permutations (Seg n) ; ::_thesis: x in Permutations n
then  x is Permutation of (Seg n) by Th1;
hence  x in Permutations n by MATRIX_2:def_9; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Permutations n or x in permutations (Seg n) )
assume  x in Permutations n ; ::_thesis: x in permutations (Seg n)
then  x is Permutation of (Seg n) by MATRIX_2:def_9;
hence  x in permutations (Seg n) ; ::_thesis: verum
end;

registration
let X be set ;
cluster permutations X ->  non empty functional ;
coherence
 ( not permutations X is empty & permutations X is functional )
proof
 the Permutation of X in permutations X ;
hence  not permutations X is empty ; ::_thesis: permutations X is functional
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in permutations X or x is set )
thus  ( not x in permutations X or x is set ) by Th1; ::_thesis: verum
end;
end;

registration
let X be finite set ;
cluster permutations X ->  finite ;
coherence
 permutations X is finite
proof
 permutations X c= Funcs (X,X) by Th2;
hence  permutations X is finite ; ::_thesis: verum
end;
end;

theorem Th4: :: CAYLEY:4
permutations {} = 1
proof
set P = permutations {};
thus  permutations {} c= 1 :: according to XBOOLE_0:def_10 ::_thesis: 1 c= permutations {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in permutations {} or x in 1 )
assume  x in permutations {} ; ::_thesis: x in 1
then  x is Permutation of {} by Th1;
hence  x in 1 by CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in 1 or x in permutations {} )
assume  x in 1 ; ::_thesis: x in permutations {}
then  x = {} ({},{}) by CARD_1:49, TARSKI:def_1;
hence  x in permutations {} ; ::_thesis: verum
end;

definition
let X be set ;
set c = permutations X;
func SymGroup X ->  strict constituted-Functions multMagma  means :Def2: :: CAYLEY:def 2
( the carrier of it = permutations X & ( for x, y being Element of it holds x * y = y * x ) );
existence
 ex b1 being strict constituted-Functions multMagma st
( the carrier of b1 = permutations X & ( for x, y being Element of b1 holds x * y = y * x ) )
proof
defpred S1[ Element of permutations X, Element of permutations X, set ] means $3 = $2 * $1;
A1: for x, y being Element of permutations X ex z being Element of permutations X st S1[x,y,z]
proof
let x, y be Element of permutations X; ::_thesis: ex z being Element of permutations X st S1[x,y,z]
reconsider f = x, g = y as Permutation of X by Th1;
 g * f in permutations X ;
hence  ex z being Element of permutations X st S1[x,y,z] ; ::_thesis: verum
end;
consider F being BinOp of (permutations X) such that
A2: for x, y being Element of permutations X holds S1[x,y,F . (x,y)] from BINOP_1:sch_3(A1);
set S = multMagma(# (permutations X),F #);
 multMagma(# (permutations X),F #) is constituted-Functions
proof
let x be Element of multMagma(# (permutations X),F #); :: according to MONOID_0:def_1 ::_thesis: x is set
thus  x is set ; ::_thesis: verum
end;
then reconsider S = multMagma(# (permutations X),F #) as strict constituted-Functions multMagma ;
take  S ; ::_thesis: ( the carrier of S = permutations X & ( for x, y being Element of S holds x * y = y * x ) )
thus  the carrier of S = permutations X ; ::_thesis: for x, y being Element of S holds x * y = y * x
let x, y be Element of S; ::_thesis: x * y = y * x
thus  x * y = y * x by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict constituted-Functions multMagma st the carrier of b1 = permutations X & ( for x, y being Element of b1 holds x * y = y * x ) & the carrier of b2 = permutations X & ( for x, y being Element of b2 holds x * y = y * x ) holds
b1 = b2
proof
let A, B be strict constituted-Functions multMagma ; ::_thesis: ( the carrier of A = permutations X & ( for x, y being Element of A holds x * y = y * x ) & the carrier of B = permutations X & ( for x, y being Element of B holds x * y = y * x ) implies A = B )
assume that
A3: the carrier of A = permutations X and
A4: for x, y being Element of A holds x * y = y * x and
A5: the carrier of B = permutations X and
A6: for x, y being Element of B holds x * y = y * x ; ::_thesis: A = B
now__::_thesis:_for_x,_y_being_Element_of_A_holds_the_multF_of_A_._(x,y)_=_the_multF_of_B_._(x,y)
let x, y be Element of A; ::_thesis: the multF of A . (x,y) = the multF of B . (x,y)
reconsider f = x, g = y as Element of B by A3, A5;
thus  the multF of A . (x,y) = x * y
.= y * x by A4
.= f * g by A6
.= the multF of B . (x,y) ; ::_thesis: verum
end;
hence  A = B by A3, A5, BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines SymGroup CAYLEY:def_2_:_
 for X being set
for b2 being strict constituted-Functions multMagma holds
( b2 = SymGroup X iff ( the carrier of b2 = permutations X & ( for x, y being Element of b2 holds x * y = y * x ) ) );

theorem Th5: :: CAYLEY:5
for X being set
for f being Element of (SymGroup X) holds f is Permutation of X
proof
let X be set ; ::_thesis: for f being Element of (SymGroup X) holds f is Permutation of X
let f be Element of (SymGroup X); ::_thesis: f is Permutation of X
 the carrier of (SymGroup X) = permutations X by Def2;
hence  f is Permutation of X by Th1; ::_thesis: verum
end;

registration
let X be set ;
cluster SymGroup X ->  non empty strict Group-like associative constituted-Functions ;
coherence
 ( not SymGroup X is empty & SymGroup X is associative & SymGroup X is Group-like )
proof
 the carrier of (SymGroup X) = permutations X by Def2;
hence  not the carrier of (SymGroup X) is empty ; :: according to STRUCT_0:def_1 ::_thesis: ( SymGroup X is associative & SymGroup X is Group-like )
thus  SymGroup X is associative ::_thesis: SymGroup X is Group-like
proof
let x, y, z be Element of (SymGroup X); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
thus (x * y) * z = z * (x * y) by Def2
.= z * (y * x) by Def2
.= (z * y) * x by RELAT_1:36
.= (y * z) * x by Def2
.= x * (y * z) by Def2 ; ::_thesis: verum
end;
set e = id X;
 id X in permutations X ;
then reconsider e = id X as Element of (SymGroup X) by Def2;
take  e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of (SymGroup X) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of (SymGroup X) st
( b1 * b2 = e & b2 * b1 = e ) )
let h be Element of (SymGroup X); ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of (SymGroup X) st
( h * b1 = e & b1 * h = e ) )
reconsider h1 = h as Permutation of X by Th5;
thus h * e = e * h1 by Def2
.= h by FUNCT_2:17 ; ::_thesis: ( e * h = h & ex b1 being Element of the carrier of (SymGroup X) st
( h * b1 = e & b1 * h = e ) )
thus e * h = h1 * e by Def2
.= h by FUNCT_2:17 ; ::_thesis: ex b1 being Element of the carrier of (SymGroup X) st
( h * b1 = e & b1 * h = e )
 h1 " in permutations X ;
then reconsider g = h1 " as Element of (SymGroup X) by Def2;
take  g ; ::_thesis: ( h * g = e & g * h = e )
thus h * g = g * h by Def2
.= e by FUNCT_2:61 ; ::_thesis: g * h = e
thus g * h = h * g by Def2
.= e by FUNCT_2:61 ; ::_thesis: verum
end;
end;

theorem Th6: :: CAYLEY:6
for X being set holds 1_ (SymGroup X) = id X
proof
let X be set ; ::_thesis: 1_ (SymGroup X) = id X
set e = id X;
 id X in permutations X ;
then reconsider e = id X as Element of (SymGroup X) by Def2;
now__::_thesis:_for_h_being_Element_of_(SymGroup_X)_holds_
(_h_*_e_=_h_&_e_*_h_=_h_)
let h be Element of (SymGroup X); ::_thesis: ( h * e = h & e * h = h )
reconsider h1 = h as Permutation of X by Th5;
thus h * e = e * h1 by Def2
.= h by FUNCT_2:17 ; ::_thesis: e * h = h
thus e * h = h1 * e by Def2
.= h by FUNCT_2:17 ; ::_thesis: verum
end;
hence  1_ (SymGroup X) = id X by GROUP_1:4; ::_thesis: verum
end;

theorem :: CAYLEY:7
for X being set
for x being Element of (SymGroup X) holds x " = x "
proof
let X be set ; ::_thesis: for x being Element of (SymGroup X) holds x " = x "
let x be Element of (SymGroup X); ::_thesis: x " = x "
reconsider f = x as Permutation of X by Th5;
 f " in permutations X ;
then reconsider g = f " as Element of (SymGroup X) by Def2;
A1: 1_ (SymGroup X) = id X by Th6;
 x * g = g * x by Def2;
then A2: x * g = id X by FUNCT_2:61;
 g * x = x * g by Def2;
then  g * x = id X by FUNCT_2:61;
hence  x " = x " by A2, A1, GROUP_1:def_5; ::_thesis: verum
end;

registration
let n be Nat;
cluster Group_of_Perm n ->  constituted-Functions ;
coherence
 Group_of_Perm n is constituted-Functions
proof
let x be set ; :: according to MONOID_0:def_1 ::_thesis: ( x is Element of the carrier of (Group_of_Perm n) implies x is set )
 the carrier of (Group_of_Perm n) = Permutations n by MATRIX_2:def_10;
hence  ( x is Element of the carrier of (Group_of_Perm n) implies x is set ) ; ::_thesis: verum
end;
end;

theorem :: CAYLEY:8
for n being Nat holds SymGroup (Seg n) = Group_of_Perm n
proof
let n be Nat; ::_thesis: SymGroup (Seg n) = Group_of_Perm n
A1: the carrier of (SymGroup (Seg n)) = permutations (Seg n) by Def2;
A2: permutations (Seg n) = Permutations n by Th3
.= the carrier of (Group_of_Perm n) by MATRIX_2:def_10 ;
now__::_thesis:_for_a,_b_being_Element_of_(SymGroup_(Seg_n))_holds_the_multF_of_(SymGroup_(Seg_n))_._(a,b)_=_the_multF_of_(Group_of_Perm_n)_._(a,b)
let a, b be Element of (SymGroup (Seg n)); ::_thesis: the multF of (SymGroup (Seg n)) . (a,b) = the multF of (Group_of_Perm n) . (a,b)
A3: a * b = b * a by Def2;
 ( a is Permutation of (Seg n) & b is Permutation of (Seg n) ) by Th5;
then  ( a in Permutations n & b in Permutations n ) by MATRIX_2:def_9;
hence  the multF of (SymGroup (Seg n)) . (a,b) = the multF of (Group_of_Perm n) . (a,b) by A3, MATRIX_2:def_10; ::_thesis: verum
end;
hence  SymGroup (Seg n) = Group_of_Perm n by A1, A2, BINOP_1:2; ::_thesis: verum
end;

registration
let X be finite set ;
cluster SymGroup X ->  finite strict constituted-Functions ;
coherence
 SymGroup X is finite
proof
 the carrier of (SymGroup X) = permutations X by Def2;
hence  the carrier of (SymGroup X) is finite ; :: according to STRUCT_0:def_11 ::_thesis: verum
end;
end;

theorem Th9: :: CAYLEY:9
SymGroup {} = Trivial-multMagma
proof
set G = SymGroup {};
A1: the carrier of (SymGroup {}) = permutations {} by Def2;
now__::_thesis:_for_x,_y_being_Element_of_1_holds_the_multF_of_(SymGroup_{})_._(x,y)_=_op2_._(x,y)
let x, y be Element of 1; ::_thesis: the multF of (SymGroup {}) . (x,y) = op2 . (x,y)
reconsider f = x, g = y as Element of (SymGroup {}) by Th4, Def2;
thus  the multF of (SymGroup {}) . (x,y) = f * g
.= {} by A1, Th4, CARD_1:49, TARSKI:def_1
.= op2 . (x,y) by CARD_1:49, FUNCOP_1:77 ; ::_thesis: verum
end;
hence  SymGroup {} = Trivial-multMagma by A1, Th4, BINOP_1:2; ::_thesis: verum
end;

registration
cluster SymGroup {} ->  trivial strict constituted-Functions ;
coherence
 SymGroup {} is trivial by Th9, CARD_1:49;
end;

definition
let X, Y be set ;
let p be Function of X,Y;
assume that
B1: ( X <> {} & Y <> {} ) and
B2: p is bijective ;
set G = SymGroup X;
set H = SymGroup Y;
func SymGroupsIso p ->  Function of (SymGroup X),(SymGroup Y) means :Def3: :: CAYLEY:def 3
 for x being Element of (SymGroup X) holds it . x = (p * x) * (p ");
existence
 ex b1 being Function of (SymGroup X),(SymGroup Y) st
for x being Element of (SymGroup X) holds b1 . x = (p * x) * (p ")
proof
A1: dom p = X by B1, FUNCT_2:def_1;
A2: rng p = Y by B2, FUNCT_2:def_3;
reconsider p1 = p " as Function of Y,X by B2, A2, FUNCT_2:25;
A3: rng p1 = X by B2, A1, FUNCT_1:33;
defpred S1[ Function, set ] means $2 = (p * $1) * p1;
A4: for x being Element of (SymGroup X) ex y being Element of (SymGroup Y) st S1[x,y]
proof
let x be Element of (SymGroup X); ::_thesis: ex y being Element of (SymGroup Y) st S1[x,y]
reconsider f = x as Permutation of X by Th5;
set y = (p * f) * p1;
 rng f = X by FUNCT_2:def_3;
then  rng (p * f) = Y by A2, B1, FUNCT_2:14;
then  rng ((p * f) * p1) = Y by B1, A3, FUNCT_2:14;
then  (p * f) * p1 is Permutation of Y by B2, B1, FUNCT_2:57;
then  (p * f) * p1 in permutations Y ;
then reconsider y = (p * f) * p1 as Element of (SymGroup Y) by Def2;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
 ex h being Function of (SymGroup X),(SymGroup Y) st
for x being Element of (SymGroup X) holds S1[x,h . x] from FUNCT_2:sch_3(A4);
hence  ex b1 being Function of (SymGroup X),(SymGroup Y) st
for x being Element of (SymGroup X) holds b1 . x = (p * x) * (p ") ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (SymGroup X),(SymGroup Y) st ( for x being Element of (SymGroup X) holds b1 . x = (p * x) * (p ") ) & ( for x being Element of (SymGroup X) holds b2 . x = (p * x) * (p ") ) holds
b1 = b2
proof
let f, g be Function of (SymGroup X),(SymGroup Y); ::_thesis: ( ( for x being Element of (SymGroup X) holds f . x = (p * x) * (p ") ) & ( for x being Element of (SymGroup X) holds g . x = (p * x) * (p ") ) implies f = g )
assume that
A5: for x being Element of (SymGroup X) holds f . x = (p * x) * (p ") and
A6: for x being Element of (SymGroup X) holds g . x = (p * x) * (p ") ; ::_thesis: f = g
let x be Element of (SymGroup X); :: according to FUNCT_2:def_8 ::_thesis: f . x = g . x
thus f . x = (p * x) * (p ") by A5
.= g . x by A6 ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines SymGroupsIso CAYLEY:def_3_:_
 for X, Y being set
for p being Function of X,Y st X <> {} & Y <> {} & p is bijective holds
for b4 being Function of (SymGroup X),(SymGroup Y) holds
( b4 = SymGroupsIso p iff for x being Element of (SymGroup X) holds b4 . x = (p * x) * (p ") );

theorem Th10: :: CAYLEY:10
for X, Y being non empty set
for p being Function of X,Y st p is bijective holds
SymGroupsIso p is multiplicative
proof
let X, Y be non empty set ; ::_thesis: for p being Function of X,Y st p is bijective holds
SymGroupsIso p is multiplicative
let p be Function of X,Y; ::_thesis: ( p is bijective implies SymGroupsIso p is multiplicative )
assume A1: p is bijective ; ::_thesis: SymGroupsIso p is multiplicative
set h = SymGroupsIso p;
A2: rng p = Y by A1, FUNCT_2:def_3;
let x, y be Element of (SymGroup X); :: according to GROUP_6:def_6 ::_thesis: (SymGroupsIso p) . (x * y) = ((SymGroupsIso p) . x) * ((SymGroupsIso p) . y)
reconsider p1 = p " as Function of Y,X by A1, A2, FUNCT_2:25;
A3: id X = p1 * p by A2, A1, FUNCT_2:29;
A4: ( (SymGroupsIso p) . x = (p * x) * p1 & (SymGroupsIso p) . y = (p * y) * p1 ) by A1, Def3;
reconsider f = x, g = y as Permutation of X by Th5;
thus (SymGroupsIso p) . (x * y) = (p * (x * y)) * p1 by A1, Def3
.= (p * (g * f)) * p1 by Def2
.= (p * ((g * (id X)) * f)) * p1 by FUNCT_2:17
.= (p * (((g * p1) * p) * f)) * p1 by A3, RELAT_1:36
.= (p * ((g * p1) * (p * f))) * p1 by RELAT_1:36
.= ((p * (g * p1)) * (p * f)) * p1 by RELAT_1:36
.= (p * (g * p1)) * ((p * f) * p1) by RELAT_1:36
.= ((p * g) * p1) * ((p * f) * p1) by RELAT_1:36
.= ((SymGroupsIso p) . x) * ((SymGroupsIso p) . y) by A4, Def2 ; ::_thesis: verum
end;

theorem Th11: :: CAYLEY:11
for X, Y being non empty set
for p being Function of X,Y st p is bijective holds
SymGroupsIso p is one-to-one
proof
let X, Y be non empty set ; ::_thesis: for p being Function of X,Y st p is bijective holds
SymGroupsIso p is one-to-one
let p be Function of X,Y; ::_thesis: ( p is bijective implies SymGroupsIso p is one-to-one )
assume A1: p is bijective ; ::_thesis: SymGroupsIso p is one-to-one
set h = SymGroupsIso p;
A2: rng p = Y by A1, FUNCT_2:def_3;
reconsider p1 = p " as Function of Y,X by A1, A2, FUNCT_2:25;
A3: id X = p1 * p by A1, A2, FUNCT_2:29;
let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom (SymGroupsIso p) or not y in dom (SymGroupsIso p) or not (SymGroupsIso p) . x = (SymGroupsIso p) . y or x = y )
assume that
A4: ( x in dom (SymGroupsIso p) & y in dom (SymGroupsIso p) ) and
A5: (SymGroupsIso p) . x = (SymGroupsIso p) . y ; ::_thesis: x = y
reconsider x = x, y = y as Element of (SymGroup X) by A4;
reconsider f = x, g = y as Permutation of X by Th5;
 ( (SymGroupsIso p) . x = (p * f) * p1 & (SymGroupsIso p) . y = (p * g) * p1 ) by A1, Def3;
then  (p * f) * (p1 * p) = ((p * g) * p1) * p by A5, RELAT_1:36;
then  (p * f) * (p1 * p) = (p * g) * (p1 * p) by RELAT_1:36;
then  p * f = (p * g) * (id X) by A3, FUNCT_2:17;
then  p1 * (p * f) = p1 * (p * g) by FUNCT_2:17;
then  (p1 * p) * f = p1 * (p * g) by RELAT_1:36;
then  (p1 * p) * f = (p1 * p) * g by RELAT_1:36;
then  f = (id X) * g by A3, FUNCT_2:17;
hence  x = y by FUNCT_2:17; ::_thesis: verum
end;

theorem Th12: :: CAYLEY:12
for X, Y being non empty set
for p being Function of X,Y st p is bijective holds
SymGroupsIso p is onto
proof
let X, Y be non empty set ; ::_thesis: for p being Function of X,Y st p is bijective holds
SymGroupsIso p is onto
let p be Function of X,Y; ::_thesis: ( p is bijective implies SymGroupsIso p is onto )
assume A1: p is bijective ; ::_thesis: SymGroupsIso p is onto
set G = SymGroup X;
set H = SymGroup Y;
set h = SymGroupsIso p;
A2: dom p = X by FUNCT_2:def_1;
thus  rng (SymGroupsIso p) c= the carrier of (SymGroup Y) ; :: according to XBOOLE_0:def_10,FUNCT_2:def_3 ::_thesis: the carrier of (SymGroup Y) c= rng (SymGroupsIso p)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of (SymGroup Y) or y in rng (SymGroupsIso p) )
assume  y in the carrier of (SymGroup Y) ; ::_thesis: y in rng (SymGroupsIso p)
then reconsider y = y as Element of (SymGroup Y) ;
reconsider g = y as Permutation of Y by Th5;
A3: rng p = Y by A1, FUNCT_2:def_3;
then reconsider p1 = p " as Function of Y,X by A1, FUNCT_2:25;
A4: id Y = p * p1 by A1, A3, FUNCT_2:29;
A5: dom (SymGroupsIso p) = the carrier of (SymGroup X) by FUNCT_2:def_1;
set x = (p1 * g) * p;
A6: rng p1 = X by A1, A2, FUNCT_1:33;
 rng g = Y by FUNCT_2:def_3;
then  rng (p1 * g) = X by A6, FUNCT_2:14;
then  rng ((p1 * g) * p) = X by A3, FUNCT_2:14;
then  (p1 * g) * p is Permutation of X by A1, FUNCT_2:57;
then  (p1 * g) * p in permutations X ;
then reconsider x = (p1 * g) * p as Element of (SymGroup X) by Def2;
(SymGroupsIso p) . x = (p * x) * p1 by A1, Def3
.= ((p * (p1 * g)) * p) * p1 by RELAT_1:36
.= (p * (p1 * g)) * (p * p1) by RELAT_1:36
.= ((id Y) * g) * (id Y) by A4, RELAT_1:36
.= g * (id Y) by FUNCT_2:17
.= y by FUNCT_2:17 ;
hence  y in rng (SymGroupsIso p) by A5, FUNCT_1:def_3; ::_thesis: verum
end;

theorem :: CAYLEY:13
for X, Y being set st X,Y are_equipotent holds
SymGroup X, SymGroup Y are_isomorphic
proof
let X, Y be set ; ::_thesis: ( X,Y are_equipotent implies SymGroup X, SymGroup Y are_isomorphic )
assume A1: X,Y are_equipotent ; ::_thesis: SymGroup X, SymGroup Y are_isomorphic
then consider p being Function such that
A2: p is one-to-one and
A3: dom p = X and
A4: rng p = Y by WELLORD2:def_4;
percases ( X = {} or X <> {} ) ;
suppose X = {} ; ::_thesis: SymGroup X, SymGroup Y are_isomorphic
hence  SymGroup X, SymGroup Y are_isomorphic by A1, CARD_1:26; ::_thesis: verum
end;
supposeA5: X <> {} ; ::_thesis: SymGroup X, SymGroup Y are_isomorphic
then A6: Y <> {} by A1, CARD_1:26;
reconsider p = p as Function of X,Y by A3, A4, FUNCT_2:2;
A7: p is onto by A4, FUNCT_2:def_3;
then reconsider h = SymGroupsIso p as Homomorphism of (SymGroup X),(SymGroup Y) by A2, A5, A6, Th10;
take  h ; :: according to GROUP_6:def_11 ::_thesis: h is bijective
thus  ( h is one-to-one & h is onto ) by A2, A5, A6, A7, Th11, Th12; :: according to FUNCT_2:def_4 ::_thesis: verum
end;
end;
end;

definition
let G be Group;
func CayleyIso G ->  Function of G,(SymGroup the carrier of G) means :Def4: :: CAYLEY:def 4
 for g being Element of G holds it . g = * g;
existence
 ex b1 being Function of G,(SymGroup the carrier of G) st
for g being Element of G holds b1 . g = * g
proof
set c = the carrier of G;
defpred S1[ Element of G, set ] means $2 = * $1;
A1: for x being Element of G ex y being Element of (SymGroup the carrier of G) st S1[x,y]
proof
let x be Element of G; ::_thesis: ex y being Element of (SymGroup the carrier of G) st S1[x,y]
set y = * x;
 * x in permutations the carrier of G ;
then reconsider y = * x as Element of (SymGroup the carrier of G) by Def2;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
 ex f being Function of G,(SymGroup the carrier of G) st
for x being Element of G holds S1[x,f . x] from FUNCT_2:sch_3(A1);
hence  ex b1 being Function of G,(SymGroup the carrier of G) st
for g being Element of G holds b1 . g = * g ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of G,(SymGroup the carrier of G) st ( for g being Element of G holds b1 . g = * g ) & ( for g being Element of G holds b2 . g = * g ) holds
b1 = b2
proof
let a, b be Function of G,(SymGroup the carrier of G); ::_thesis: ( ( for g being Element of G holds a . g = * g ) & ( for g being Element of G holds b . g = * g ) implies a = b )
assume that
A2: for g being Element of G holds a . g = * g and
A3: for g being Element of G holds b . g = * g ; ::_thesis: a = b
let x be Element of G; :: according to FUNCT_2:def_8 ::_thesis: a . x = b . x
thus a . x = * x by A2
.= b . x by A3 ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines CayleyIso CAYLEY:def_4_:_
 for G being Group
for b2 being Function of G,(SymGroup the carrier of G) holds
( b2 = CayleyIso G iff for g being Element of G holds b2 . g = * g );

registration
let G be Group;
cluster CayleyIso G ->  multiplicative ;
coherence
 CayleyIso G is multiplicative
proof
set c = the carrier of G;
set f = CayleyIso G;
let g1, g2 be Element of G; :: according to GROUP_6:def_6 ::_thesis: (CayleyIso G) . (g1 * g2) = ((CayleyIso G) . g1) * ((CayleyIso G) . g2)
A1: (CayleyIso G) . (g1 * g2) is Permutation of the carrier of G by Th5;
then A2: dom ((CayleyIso G) . (g1 * g2)) = the carrier of G by FUNCT_2:def_1;
 ((CayleyIso G) . g1) * ((CayleyIso G) . g2) is Permutation of the carrier of G by Th5;
then A3: dom (((CayleyIso G) . g1) * ((CayleyIso G) . g2)) = the carrier of G by FUNCT_2:def_1;
now__::_thesis:_for_y_being_set_st_y_in_dom_((CayleyIso_G)_._(g1_*_g2))_holds_
((CayleyIso_G)_._(g1_*_g2))_._y_=_(((CayleyIso_G)_._g1)_*_((CayleyIso_G)_._g2))_._y
let y be set ; ::_thesis: ( y in dom ((CayleyIso G) . (g1 * g2)) implies ((CayleyIso G) . (g1 * g2)) . y = (((CayleyIso G) . g1) * ((CayleyIso G) . g2)) . y )
assume  y in dom ((CayleyIso G) . (g1 * g2)) ; ::_thesis: ((CayleyIso G) . (g1 * g2)) . y = (((CayleyIso G) . g1) * ((CayleyIso G) . g2)) . y
then reconsider x = y as Element of G by A1, FUNCT_2:def_1;
thus ((CayleyIso G) . (g1 * g2)) . y = (* (g1 * g2)) . x by Def4
.= x * (g1 * g2) by TOPGRP_1:def_2
.= (x * g1) * g2 by GROUP_1:def_3
.= (* g2) . (x * g1) by TOPGRP_1:def_2
.= (* g2) . ((* g1) . x) by TOPGRP_1:def_2
.= ((* g2) * (* g1)) . x by FUNCT_2:15
.= (((CayleyIso G) . g2) * (* g1)) . x by Def4
.= (((CayleyIso G) . g2) * ((CayleyIso G) . g1)) . y by Def4
.= (((CayleyIso G) . g1) * ((CayleyIso G) . g2)) . y by Def2 ; ::_thesis: verum
end;
hence  (CayleyIso G) . (g1 * g2) = ((CayleyIso G) . g1) * ((CayleyIso G) . g2) by A2, A3, FUNCT_1:2; ::_thesis: verum
end;
end;

registration
let G be Group;
cluster CayleyIso G ->  one-to-one ;
coherence
 CayleyIso G is one-to-one
proof
set f = CayleyIso G;
let g1, g2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not g1 in dom (CayleyIso G) or not g2 in dom (CayleyIso G) or not (CayleyIso G) . g1 = (CayleyIso G) . g2 or g1 = g2 )
assume that
A1: ( g1 in dom (CayleyIso G) & g2 in dom (CayleyIso G) ) and
A2: (CayleyIso G) . g1 = (CayleyIso G) . g2 and
A3: g1 <> g2 ; ::_thesis: contradiction
reconsider g1 = g1, g2 = g2 as Element of G by A1;
A4: ( (CayleyIso G) . g1 = * g1 & (CayleyIso G) . g2 = * g2 ) by Def4;
A5: dom (* g1) = the carrier of G by FUNCT_2:def_1;
A6: g1 " <> g2 " by A3, GROUP_1:9;
A7: (* g1) . (g1 ") = (g1 ") * g1 by TOPGRP_1:def_2
.= 1_ G by GROUP_1:def_5 ;
(* g2) . (g2 ") = (g2 ") * g2 by TOPGRP_1:def_2
.= 1_ G by GROUP_1:def_5 ;
hence  contradiction by A2, A4, A5, A6, A7, FUNCT_1:def_4; ::_thesis: verum
end;
end;

theorem :: CAYLEY:14
for G being Group holds G, Image (CayleyIso G) are_isomorphic by GROUP_6:68;