let G be finite Group; :: thesis: for a being Element of G
for x being Element of con_class a holds card (() " {x}) = card ()

let a be Element of G; :: thesis: for x being Element of con_class a holds card (() " {x}) = card ()
let x be Element of con_class a; :: thesis: card (() " {x}) = card ()
ex b being Element of G st
( b = x & a,b are_conjugated ) by GROUP_3:80;
then consider d being Element of G such that
A1: x = a |^ d by GROUP_3:74;
reconsider Cad = () * d as Subset of G ;
A2: ex B, C being finite set st
( B = d * () & C = Cad & card () = card B & card () = card C ) by GROUP_2:133;
for g being object holds
( g in () " {x} iff g in Cad )
proof
let g be object ; :: thesis: ( g in () " {x} iff g in Cad )
A3: now :: thesis: ( g in () " {x} implies g in Cad )
assume A4: g in () " {x} ; :: thesis: g in Cad
then (a -con_map) . g in {x} by FUNCT_1:def 7;
then A5: (a -con_map) . g = x by TARSKI:def 1;
reconsider y = g as Element of G by A4;
A6: (a -con_map) . g = a |^ y by Def2;
A7: y * (((d ") * a) * d) = (y * ((d ") * a)) * d by GROUP_1:def 3
.= ((y * (d ")) * a) * d by GROUP_1:def 3 ;
y * (((y ") * a) * y) = (y * ((y ") * a)) * y by GROUP_1:def 3
.= a * y by GROUP_3:1 ;
then (((y * (d ")) * a) * d) * (d ") = a * (y * (d ")) by ;
then (y * (d ")) * a = a * (y * (d ")) by GROUP_3:1;
then y * (d ") is Element of () by Th8;
then consider z being Element of G such that
A8: z in the carrier of () and
A9: y * (d ") = z ;
A10: z in Centralizer a by A8;
reconsider z = z as Element of G ;
y = z * d by ;
hence g in Cad by ; :: thesis: verum
end;
now :: thesis: ( g in Cad implies g in () " {x} )
assume g in Cad ; :: thesis: g in () " {x}
then consider z being Element of G such that
A11: g = z * d and
A12: z in Centralizer a by GROUP_2:104;
reconsider y = g as Element of G by A11;
y * (d ") = z by ;
then y * (d ") in carr () by A12;
then (y * (d ")) * a = a * (y * (d ")) by Th8;
then ((y * (d ")) * a) * d = a * ((y * (d ")) * d) by GROUP_1:def 3;
then ((y * (d ")) * a) * d = a * y by GROUP_3:1;
then (y * (d ")) * (a * d) = a * y by GROUP_1:def 3;
then (y ") * ((y * (d ")) * (a * d)) = ((y ") * a) * y by GROUP_1:def 3;
then ((y ") * (y * (d "))) * (a * d) = ((y ") * a) * y by GROUP_1:def 3;
then (d ") * (a * d) = ((y ") * a) * y by GROUP_3:1;
then x = a |^ y by ;
then (a -con_map) . y = x by Def2;
then A13: (a -con_map) . y in {x} by TARSKI:def 1;
dom () = the carrier of G by FUNCT_2:def 1;
hence g in () " {x} by ; :: thesis: verum
end;
hence ( g in () " {x} iff g in Cad ) by A3; :: thesis: verum
end;
hence card (() " {x}) = card () by ; :: thesis: verum