let G be Group; :: thesis: for N being normal Subgroup of G
for A being Element of Cosets N
for g being Element of G holds
( g in A iff A = g * N )
let N be normal Subgroup of G; :: thesis: for A being Element of Cosets N
for g being Element of G holds
( g in A iff A = g * N )
let A be Element of Cosets N; :: thesis: for g being Element of G holds
( g in A iff A = g * N )
let g be Element of G; :: thesis: ( g in A iff A = g * N )

hereby :: thesis: ( A = g * N implies g in A )

consider a being Element of G such that
A1: A = a * N by GROUP_2:def 15;
assume g in A ; :: thesis: A = g * N
then consider h being Element of G such that
A2: g = a * h and
A3: h in N by A1, GROUP_2:103;
(g ") * a = ((h ") * (a ")) * a by A2, GROUP_1:17
.= (h ") * ((a ") * a) by GROUP_1:def 3
.= (h ") * (1_ G) by GROUP_1:def 5
.= h " by GROUP_1:def 4 ;
then (g ") * a in N by A3, GROUP_2:51;
hence A = g * N by A1, GROUP_2:114; :: thesis: verum

end;

( g = g * (1_ G) & 1_ G in N ) by GROUP_1:def 4, GROUP_2:46;
hence ( A = g * N implies g in A ) by GROUP_2:103; :: thesis: verum