let G be finite Group; :: thesis: for a being Element of G
for x being Element of con_class a holds card ((a -con_map) " {x}) = card (Centralizer a)
let a be Element of G; :: thesis: for x being Element of con_class a holds card ((a -con_map) " {x}) = card (Centralizer a)
let x be Element of con_class a; :: thesis: card ((a -con_map) " {x}) = card (Centralizer a)
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 = (Centralizer a) * d as Subset of G ;
A2: ex B, C being finite set st
( B = d * (Centralizer a) & C = Cad & card (Centralizer a) = card B & card (Centralizer a) = card C ) by GROUP_2:133;
for g being object holds
( g in (a -con_map) " {x} iff g in Cad )

proof

let g be object ; :: thesis: ( g in (a -con_map) " {x} iff g in Cad )

A3: now :: thesis: ( g in (a -con_map) " {x} implies g in Cad )

assume A4: g in (a -con_map) " {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 A1, A5, A6, A7, GROUP_1:def 3;
then (y * (d ")) * a = a * (y * (d ")) by GROUP_3:1;
then y * (d ") is Element of (Centralizer a) by Th8;
then consider z being Element of G such that
A8: z in the carrier of (Centralizer a) and
A9: y * (d ") = z ;
A10: z in Centralizer a by A8;
reconsider z = z as Element of G ;
y = z * d by A9, GROUP_3:1;
hence g in Cad by A10, GROUP_2:104; :: thesis: verum

end;

now :: thesis: ( g in Cad implies g in (a -con_map) " {x} )

assume g in Cad ; :: thesis: g in (a -con_map) " {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 A11, GROUP_3:1;
then y * (d ") in carr (Centralizer a) 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 A1, GROUP_1:def 3;
then (a -con_map) . y = x by Def2;
then A13: (a -con_map) . y in {x} by TARSKI:def 1;
dom (a -con_map) = the carrier of G by FUNCT_2:def 1;
hence g in (a -con_map) " {x} by A13, FUNCT_1:def 7; :: thesis: verum

end;

hence ( g in (a -con_map) " {x} iff g in Cad ) by A3; :: thesis: verum

end;

hence card ((a -con_map) " {x}) = card (Centralizer a) by A2, TARSKI:2; :: thesis: verum