let G be addGroup; :: thesis: for H being Subgroup of G st Left_Cosets H is finite & index H = 2 holds
H is normal Subgroup of G
let H be Subgroup of G; :: thesis: ( Left_Cosets H is finite & index H = 2 implies H is normal Subgroup of G )
assume that
A1: Left_Cosets H is finite and
A2: index H = 2 ; :: thesis: H is normal Subgroup of G
ex B being finite set st
( B = Left_Cosets H & index H = card B ) by A1, Th146;
then consider x, y being object such that
A3: x <> y and
A4: Left_Cosets H = {x,y} by A2, CARD_2:60;
carr H in Left_Cosets H by Th135;
then ( {x,y} = {x,(carr H)} or {x,y} = {(carr H),y} ) by A4, TARSKI:def 2;
then consider z3 being object such that
A5: {x,y} = {(carr H),z3} ;
reconsider z3 = z3 as set by TARSKI:1;
A6: carr H misses z3

proof

z3 in Left_Cosets H by A4, A5, TARSKI:def 2;
then A7: ex a being Element of G st z3 = a + H by Def15;
A8: carr H = (0_ G) + H by ThB109;
assume not carr H misses z3 ; :: thesis: contradiction
then carr H = z3 by A7, A8, Th115;
then A9: {x,y} = {(carr H)} by A5, ENUMSET1:29;
then x = carr H by ZFMISC_1:4;
hence contradiction by A3, A9, ZFMISC_1:4; :: thesis: verum

end;

( union (Left_Cosets H) = the carrier of G & union (Left_Cosets H) = (carr H) \/ z3 ) by A4, A5, Th137, ZFMISC_1:75;
then A10: ( union (Right_Cosets H) = the carrier of G & z3 = the carrier of G \ (carr H) ) by A6, Th137, XBOOLE_1:88;
ex C being finite set st
( C = Right_Cosets H & index H = card C ) by A1, Th146;
then consider z1, z2 being object such that
A11: z1 <> z2 and
A12: Right_Cosets H = {z1,z2} by A2, CARD_2:60;
carr H in Right_Cosets H by Th135;
then ( {z1,z2} = {z1,(carr H)} or {z1,z2} = {(carr H),z2} ) by A12, TARSKI:def 2;
then consider z4 being object such that
A13: {z1,z2} = {(carr H),z4} ;
reconsider z4 = z4 as set by TARSKI:1;
A14: carr H misses z4

proof

z4 in Right_Cosets H by A12, A13, TARSKI:def 2;
then A15: ex a being Element of G st z4 = H + a by Def16;
A16: carr H = H + (0_ G) by ThB109;
assume not carr H misses z4 ; :: thesis: contradiction
then carr H = z4 by A15, A16, Th121;
then A17: {z1,z2} = {(carr H)} by A13, ENUMSET1:29;
then z1 = carr H by ZFMISC_1:4;
hence contradiction by A11, A17, ZFMISC_1:4; :: thesis: verum

end;

A18: union (Right_Cosets H) = (carr H) \/ z4 by A12, A13, ZFMISC_1:75;

now :: thesis: for c being Element of G holds c + H = H + c

let c be Element of G; :: thesis: c + H = H + c

now :: thesis: c + H = H + c

per cases ( c + H = carr H or c + H <> carr H ) ;

suppose c + H = carr H ; :: thesis: c + H = H + c

hence c + H = H + c by Th113, Th119; :: thesis: verum

end;

suppose A20: c + H <> carr H ; :: thesis: c + H = H + c

then A21: H + c <> carr H by Th113, Th119;
c + H in Left_Cosets H by Def15;
then A22: c + H = z3 by A4, A5, A20, TARSKI:def 2;
H + c in Right_Cosets H by Def16;
then H + c = z4 by A12, A13, A21, TARSKI:def 2;
hence c + H = H + c by A10, A18, A14, A22, XBOOLE_1:88; :: thesis: verum

end;

end;

end;

hence c + H = H + c ; :: thesis: verum

end;

hence H is normal Subgroup of G by Th117; :: thesis: verum