let G be finite Group; :: thesis: for H1, H2 being strict Subgroup of G st H1,H2 are_isomorphic holds
index H1 = index H2
let H1, H2 be strict Subgroup of G; :: thesis: ( H1,H2 are_isomorphic implies index H1 = index H2 )
assume A1: H1,H2 are_isomorphic ; :: thesis: index H1 = index H2
(card H1) * (index H1) = card G by GROUP_2:147
.= (card H2) * (index H2) by GROUP_2:147 ;
then (index H1) * (card H1) = (index H2) * (card H1) by A1, GROUP_6:73;
hence index H1 = index H2 by XCMPLX_1:5; :: thesis: verum