for G being finite Group
for a being Element of G
for x being Element of con_class a holds card ((a -con_map) " {x}) = card (Centralizer a)