let G be finite addGroup; :: thesis: for H being strict Subgroup of G st index H = card G holds
H = (0). G
let H be strict Subgroup of G; :: thesis: ( index H = card G implies H = (0). G )
assume index H = card G ; :: thesis: H = (0). G
then 1 * (card G) = (card H) * (card G) by Th147;
hence H = (0). G by Th70, XCMPLX_1:5; :: thesis: verum