let G be Group; :: thesis: for E being non empty set
for a being Element of E
for T being LeftOperation of G,E holds card (the_orbit_of (a,T)) = Index (the_strict_stabilizer_of (a,T))
let E be non empty set ; :: thesis: for a being Element of E
for T being LeftOperation of G,E holds card (the_orbit_of (a,T)) = Index (the_strict_stabilizer_of (a,T))
let a be Element of E; :: thesis: for T being LeftOperation of G,E holds card (the_orbit_of (a,T)) = Index (the_strict_stabilizer_of (a,T))
let T be LeftOperation of G,E; :: thesis: card (the_orbit_of (a,T)) = Index (the_strict_stabilizer_of (a,T))
set H = the_strict_stabilizer_of (a,T);
set f = { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } ;
reconsider A9 = {a} as Subset of E ;

A1: now :: thesis: for x being object st x in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } holds
ex b, A being object st x = [b,A]

let x be object ; :: thesis: ( x in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } implies ex b, A being object st x = [b,A] )
assume x in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } ; :: thesis: ex b, A being object st x = [b,A]
then consider b being Element of E, A being Subset of G such that
A2: [b,A] = x and
ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) ;
reconsider b = b, A = A as object ;
take b = b; :: thesis: ex A being object st x = [b,A]
take A = A; :: thesis: x = [b,A]
thus x = [b,A] by A2; :: thesis: verum

end;

now :: thesis: for x, y1, y2 being object st [x,y1] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } & [x,y2] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } holds
y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } & [x,y2] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } implies y1 = y2 )
assume [x,y1] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } ; :: thesis: ( [x,y2] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } implies y1 = y2 )
then consider b1 being Element of E, A1 being Subset of G such that
A3: [b1,A1] = [x,y1] and
A4: ex g being Element of G st
( b1 = (T ^ g) . a & A1 = g * (the_strict_stabilizer_of (a,T)) ) ;
assume [x,y2] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } ; :: thesis: y1 = y2
then consider b2 being Element of E, A2 being Subset of G such that
A5: [b2,A2] = [x,y2] and
A6: ex g being Element of G st
( b2 = (T ^ g) . a & A2 = g * (the_strict_stabilizer_of (a,T)) ) ;
A7: y2 = A2 by A5, XTUPLE_0:1;
consider g1 being Element of G such that
A8: b1 = (T ^ g1) . a and
A9: A1 = g1 * (the_strict_stabilizer_of (a,T)) by A4;
consider g2 being Element of G such that
A10: b2 = (T ^ g2) . a and
A11: A2 = g2 * (the_strict_stabilizer_of (a,T)) by A6;
x = b2 by A5, XTUPLE_0:1;
then ( dom (T ^ g1) = E & (T ^ g1) . a = (T ^ g2) . a ) by A3, A8, A10, FUNCT_2:def 1, XTUPLE_0:1;
then ( dom (T ^ g2) = E & Im ((T ^ g1),a) = {((T ^ g2) . a)} ) by FUNCT_1:59, FUNCT_2:def 1;
then A12: Im ((T ^ g1),a) = Im ((T ^ g2),a) by FUNCT_1:59;
set g = (g2 ") * g1;
reconsider g = (g2 ") * g1 as Element of G ;
A13: the carrier of (the_strict_stabilizer_of (A9,T)) = { g9 where g9 is Element of G : (T ^ g9) .: A9 = A9 } by Def10;
(T ^ g) .: A9 = ((T ^ (g2 ")) * (T ^ g1)) .: A9 by Def1
.= (T ^ (g2 ")) .: ((T ^ g1) .: A9) by RELAT_1:126
.= ((T ^ (g2 ")) * (T ^ g2)) .: A9 by A12, RELAT_1:126
.= (T ^ ((g2 ") * g2)) .: A9 by Def1
.= (T ^ (1_ G)) .: A9 by GROUP_1:def 5
.= (id E) .: A9 by Def1
.= A9 by FUNCT_1:92 ;
then g in { g9 where g9 is Element of G : (T ^ g9) .: A9 = A9 } ;
then A14: g in the_strict_stabilizer_of (A9,T) by A13;
y1 = A1 by A3, XTUPLE_0:1;
hence y1 = y2 by A7, A9, A11, A14, GROUP_2:114; :: thesis: verum

end;

then reconsider f = { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } as Function by A1, FUNCT_1:def 1, RELAT_1:def 1;
for y being object holds
( y in Left_Cosets (the_strict_stabilizer_of (a,T)) iff ex x being object st [x,y] in f )

proof

let y be object ; :: thesis: ( y in Left_Cosets (the_strict_stabilizer_of (a,T)) iff ex x being object st [x,y] in f )

hereby :: thesis: ( ex x being object st [x,y] in f implies y in Left_Cosets (the_strict_stabilizer_of (a,T)) )

assume A15: y in Left_Cosets (the_strict_stabilizer_of (a,T)) ; :: thesis: ex x being object st [x,y] in f
then reconsider A = y as Subset of G ;
consider g being Element of G such that
A16: A = g * (the_strict_stabilizer_of (a,T)) by A15, GROUP_2:def 15;
reconsider x = (T ^ g) . a as object ;
take x = x; :: thesis: [x,y] in f
thus [x,y] in f by A16; :: thesis: verum

end;

given x being object such that A17: [x,y] in f ; :: thesis: y in Left_Cosets (the_strict_stabilizer_of (a,T))
consider b being Element of E, A being Subset of G such that
A18: [b,A] = [x,y] and
A19: ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) by A17;
A = y by A18, XTUPLE_0:1;
hence y in Left_Cosets (the_strict_stabilizer_of (a,T)) by A19, GROUP_2:def 15; :: thesis: verum

end;

then A20: rng f = Left_Cosets (the_strict_stabilizer_of (a,T)) by XTUPLE_0:def 13;

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
A21: the carrier of (the_strict_stabilizer_of (A9,T)) = { g9 where g9 is Element of G : (T ^ g9) .: A9 = A9 } by Def10;
assume x1 in dom f ; :: thesis: ( x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
then [x1,(f . x1)] in f by FUNCT_1:1;
then consider b1 being Element of E, A1 being Subset of G such that
A22: [b1,A1] = [x1,(f . x1)] and
A23: ex g being Element of G st
( b1 = (T ^ g) . a & A1 = g * (the_strict_stabilizer_of (a,T)) ) ;
assume x2 in dom f ; :: thesis: ( f . x1 = f . x2 implies x1 = x2 )
then [x2,(f . x2)] in f by FUNCT_1:1;
then consider b2 being Element of E, A2 being Subset of G such that
A24: [b2,A2] = [x2,(f . x2)] and
A25: ex g being Element of G st
( b2 = (T ^ g) . a & A2 = g * (the_strict_stabilizer_of (a,T)) ) ;
consider g2 being Element of G such that
A26: b2 = (T ^ g2) . a and
A27: A2 = g2 * (the_strict_stabilizer_of (a,T)) by A25;
assume A28: f . x1 = f . x2 ; :: thesis: x1 = x2
consider g1 being Element of G such that
A29: b1 = (T ^ g1) . a and
A30: A1 = g1 * (the_strict_stabilizer_of (a,T)) by A23;
set g = (g2 ") * g1;
f . x2 = A2 by A24, XTUPLE_0:1;
then g1 * (the_strict_stabilizer_of (a,T)) = g2 * (the_strict_stabilizer_of (a,T)) by A22, A30, A27, A28, XTUPLE_0:1;
then (g2 ") * g1 in the_strict_stabilizer_of (a,T) by GROUP_2:114;
then (g2 ") * g1 in the carrier of (the_strict_stabilizer_of (A9,T)) ;
then A31: ex g9 being Element of G st
( (g2 ") * g1 = g9 & (T ^ g9) .: A9 = A9 ) by A21;
(T ^ g1) .: A9 = (id E) .: ((T ^ g1) .: A9) by FUNCT_1:92
.= (T ^ (1_ G)) .: ((T ^ g1) .: A9) by Def1
.= (T ^ (g2 * (g2 "))) .: ((T ^ g1) .: A9) by GROUP_1:def 5
.= ((T ^ (g2 * (g2 "))) * (T ^ g1)) .: A9 by RELAT_1:126
.= (T ^ ((g2 * (g2 ")) * g1)) .: A9 by Def1
.= (T ^ (g2 * ((g2 ") * g1))) .: A9 by GROUP_1:def 3
.= ((T ^ g2) * (T ^ ((g2 ") * g1))) .: A9 by Def1
.= (T ^ g2) .: A9 by A31, RELAT_1:126 ;
then ( dom (T ^ g2) = E & Im ((T ^ g1),a) = Im ((T ^ g2),a) ) by FUNCT_2:def 1;
then ( dom (T ^ g1) = E & Im ((T ^ g1),a) = {((T ^ g2) . a)} ) by FUNCT_1:59, FUNCT_2:def 1;
then A32: {((T ^ g1) . a)} = {((T ^ g2) . a)} by FUNCT_1:59;
A33: x2 = b2 by A24, XTUPLE_0:1;
x1 = b1 by A22, XTUPLE_0:1;
hence x1 = x2 by A33, A29, A26, A32, ZFMISC_1:18; :: thesis: verum

end;

then A34: f is one-to-one by FUNCT_1:def 4;
for x being object holds
( x in the_orbit_of (a,T) iff ex y being object st [x,y] in f )

proof

let x be object ; :: thesis: ( x in the_orbit_of (a,T) iff ex y being object st [x,y] in f )

hereby :: thesis: ( ex y being object st [x,y] in f implies x in the_orbit_of (a,T) )

assume x in the_orbit_of (a,T) ; :: thesis: ex y being object st [x,y] in f
then consider b being Element of E such that
A35: b = x and
A36: a,b are_conjugated_under T ;
consider g being Element of G such that
A37: b = (T ^ g) . a by A36;
reconsider y = g * (the_strict_stabilizer_of (a,T)) as object ;
take y = y; :: thesis: [x,y] in f
thus [x,y] in f by A35, A37; :: thesis: verum

end;

given y being object such that A38: [x,y] in f ; :: thesis: x in the_orbit_of (a,T)
consider b being Element of E, A being Subset of G such that
A39: ( [b,A] = [x,y] & ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) ) by A38;
( b = x & a,b are_conjugated_under T ) by A39, XTUPLE_0:1;
hence x in the_orbit_of (a,T) ; :: thesis: verum

end;

then dom f = the_orbit_of (a,T) by XTUPLE_0:def 12;
then the_orbit_of (a,T), Left_Cosets (the_strict_stabilizer_of (a,T)) are_equipotent by A34, A20;
hence card (the_orbit_of (a,T)) = Index (the_strict_stabilizer_of (a,T)) by CARD_1:5; :: thesis: verum