theorem Th69: :: GROUP_22:64

for G1, G2 being finite Group
for N1 being normal Subgroup of G1
for N2 being normal Subgroup of G2 st G1 ./. N1,G2 ./. N2 are_isomorphic holds
(card N2) * (card G1) = (card N1) * (card G2)