for G being finite Group
for a being Element of G holds card G = (card (con_class a)) * (card (Centralizer a))