let G be addGroup; :: thesis: for H being strict Subgroup of G st Left_Cosets H is finite & Index H = card G holds
( G is finite & H = (0). G )
let H be strict Subgroup of G; :: thesis: ( Left_Cosets H is finite & Index H = card G implies ( G is finite & H = (0). G ) )
assume that
A1: Left_Cosets H is finite and
A2: Index H = card G ; :: thesis: ( G is finite & H = (0). G )
thus A3: G is finite by A1, A2; :: thesis: H = (0). G
ex B being finite set st
( B = Left_Cosets H & index H = card B ) by A1, Def18;
hence H = (0). G by A2, A3, Th154; :: thesis: verum