let G be Group; :: thesis: for H being strict Subgroup of G st Left_Cosets H is finite & Index H = card G holds

( G is finite & H = (1). G )

let H be strict Subgroup of G; :: thesis: ( Left_Cosets H is finite & Index H = card G implies ( G is finite & H = (1). G ) )

assume that

A1: Left_Cosets H is finite and

A2: Index H = card G ; :: thesis: ( G is finite & H = (1). G )

thus A3: G is finite by A1, A2; :: thesis: H = (1). G

ex B being finite set st

( B = Left_Cosets H & index H = card B ) by A1, Def18;

hence H = (1). G by A2, A3, Th154; :: thesis: verum

( G is finite & H = (1). G )

let H be strict Subgroup of G; :: thesis: ( Left_Cosets H is finite & Index H = card G implies ( G is finite & H = (1). G ) )

assume that

A1: Left_Cosets H is finite and

A2: Index H = card G ; :: thesis: ( G is finite & H = (1). G )

thus A3: G is finite by A1, A2; :: thesis: H = (1). G

ex B being finite set st

( B = Left_Cosets H & index H = card B ) by A1, Def18;

hence H = (1). G by A2, A3, Th154; :: thesis: verum