theorem Th70: :: GROUP_22:65

for G being finite Group
for K, N being strict normal Subgroup of G
for m, d being Nat st m = card N & m = card K & d = card (K /\ N) holds
d * (card (N "\/" K)) = m * m