let G1, G2 be finite Group; :: thesis: 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)
let N1 be normal Subgroup of G1; :: thesis: for N2 being normal Subgroup of G2 st G1 ./. N1,G2 ./. N2 are_isomorphic holds
(card N2) * (card G1) = (card N1) * (card G2)
let N2 be normal Subgroup of G2; :: thesis: ( G1 ./. N1,G2 ./. N2 are_isomorphic implies (card N2) * (card G1) = (card N1) * (card G2) )
assume G1 ./. N1,G2 ./. N2 are_isomorphic ; :: thesis: (card N2) * (card G1) = (card N1) * (card G2)
then A1: card (G1 ./. N1) = card (G2 ./. N2) by GROUP_6:73
.= index N2 by GROUP_6:27 ;
set k = index N1;
A2: card G1 = (card N1) * (index N1) by GROUP_2:147
.= (card N1) * (index N1) ;
card G2 = (card N2) * (index N2) by GROUP_2:147
.= (card N2) * (index N1) by A1, GROUP_6:27 ;
hence (card N2) * (card G1) = (card N1) * (card G2) by A2; :: thesis: verum