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

H = G

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

assume that

A1: Left_Cosets H is finite and

A2: index H = 1 ; :: thesis: H = G

reconsider B = Left_Cosets H as finite set by A1;

card B = 1 by A2, Def18;

then consider x being object such that

A3: Left_Cosets H = {x} by CARD_2:42;

( union {x} = x & union (Left_Cosets H) = the carrier of G ) by Th137, ZFMISC_1:25;

hence H = G by A3, Th143; :: thesis: verum

H = G

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

assume that

A1: Left_Cosets H is finite and

A2: index H = 1 ; :: thesis: H = G

reconsider B = Left_Cosets H as finite set by A1;

card B = 1 by A2, Def18;

then consider x being object such that

A3: Left_Cosets H = {x} by CARD_2:42;

( union {x} = x & union (Left_Cosets H) = the carrier of G ) by Th137, ZFMISC_1:25;

hence H = G by A3, Th143; :: thesis: verum