let G be strict addGroup; :: 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