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

let x be set ; :: 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 set 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 set 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 set ;
take b = b; :: thesis: ex A being set st x = [b,A]
take A = A; :: thesis: x = [b,A]
thus x = [b,A] by A2; :: thesis: verum

end;

now

let x, y1, y2 be set ; :: 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, ZFMISC_1:33;
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, ZFMISC_1:33;
then ( dom (T ^ g1) = E & (T ^ g1) . a = (T ^ g2) . a ) by A3, A8, A10, FUNCT_2:def 1, ZFMISC_1:33;
then ( dom (T ^ g2) = E & Im (T ^ g1),a = {((T ^ g2) . a)} ) by FUNCT_1:117, FUNCT_2:def 1;
then A12: Im (T ^ g1),a = Im (T ^ g2),a by FUNCT_1:117;
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:159
.= ((T ^ (g2 " )) * (T ^ g2)) .: A9 by A12, RELAT_1:159
.= (T ^ ((g2 " ) * g2)) .: A9 by Def1
.= (T ^ (1_ G)) .: A9 by GROUP_1:def 6
.= (id E) .: A9 by Def1
.= A9 by FUNCT_1:162 ;
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, STRUCT_0:def 5;
y1 = A1 by A3, ZFMISC_1:33;
hence y1 = y2 by A7, A9, A11, A14, GROUP_2:137; :: 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 set holds
( y in Left_Cosets (the_strict_stabilizer_of a,T) iff ex x being set st [x,y] in f )

proof

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

hereby :: thesis: ( ex x being set 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 set 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 set ;
take x = x; :: thesis: [x,y] in f
thus [x,y] in f by A16; :: thesis: verum

end;

given x being set 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, ZFMISC_1:33;
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 RELAT_1:def 5;

now

let x1, x2 be set ; :: 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:8;
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:8;
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, ZFMISC_1:33;
then g1 * (the_strict_stabilizer_of a,T) = g2 * (the_strict_stabilizer_of a,T) by A22, A30, A27, A28, ZFMISC_1:33;
then (g2 " ) * g1 in the_strict_stabilizer_of a,T by GROUP_2:137;
then (g2 " ) * g1 in the carrier of (the_strict_stabilizer_of A9,T) by STRUCT_0:def 5;
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:162
.= (T ^ (1_ G)) .: ((T ^ g1) .: A9) by Def1
.= (T ^ (g2 * (g2 " ))) .: ((T ^ g1) .: A9) by GROUP_1:def 6
.= ((T ^ (g2 * (g2 " ))) * (T ^ g1)) .: A9 by RELAT_1:159
.= (T ^ ((g2 * (g2 " )) * g1)) .: A9 by Def1
.= (T ^ (g2 * ((g2 " ) * g1))) .: A9 by GROUP_1:def 4
.= ((T ^ g2) * (T ^ ((g2 " ) * g1))) .: A9 by Def1
.= (T ^ g2) .: A9 by A31, RELAT_1:159 ;
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:117, FUNCT_2:def 1;
then A32: {((T ^ g1) . a)} = {((T ^ g2) . a)} by FUNCT_1:117;
A33: x2 = b2 by A24, ZFMISC_1:33;
x1 = b1 by A22, ZFMISC_1:33;
hence x1 = x2 by A33, A29, A26, A32, ZFMISC_1:24; :: thesis: verum

end;

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

proof

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

hereby :: thesis: ( ex y being set 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 set 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, Def14;
reconsider y = g * (the_strict_stabilizer_of a,T) as set ;
take y = y; :: thesis: [x,y] in f
thus [x,y] in f by A35, A37; :: thesis: verum

end;

given y being set 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, Def14, ZFMISC_1:33;
hence x in the_orbit_of a,T ; :: thesis: verum

end;

then dom f = the_orbit_of a,T by RELAT_1:def 4;
then the_orbit_of a,T, Left_Cosets (the_strict_stabilizer_of a,T) are_equipotent by A34, A20, WELLORD2:def 4;
hence card (the_orbit_of a,T) = Index (the_strict_stabilizer_of a,T) by CARD_1:21; :: thesis: verum