theorem :: WEDDWITT:14

for G being finite Group
for f being FinSequence of conjugate_Classes G st f is one-to-one & rng f = conjugate_Classes G holds
for c being FinSequence of NAT st len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) holds
card G = Sum c by Th6;