let G be finite Group; :: thesis: for H being strict Subgroup of G st index H = card G holds
H = (1). G
let H be strict Subgroup of G; :: thesis: ( index H = card G implies H = (1). G )
assume index H = card G ; :: thesis: H = (1). G
then ( 1 * (card G) = (card H) * (card G) & card G <> 0 ) by Th177;
hence H = (1). G by Th82, XCMPLX_1:5; :: thesis: verum