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:125;
(g " ) * a = ((h " ) * (a " )) * a by A2, GROUP_1:25
.= (h " ) * ((a " ) * a) by GROUP_1:def 4
.= (h " ) * (1_ G) by GROUP_1:def 6
.= h " by GROUP_1:def 5 ;
then (g " ) * a in N by A3, GROUP_2:60;
hence A = g * N by A1, GROUP_2:137; :: thesis: verum

end;

( g = g * (1_ G) & 1_ G in N ) by GROUP_1:def 5, GROUP_2:55;
hence ( A = g * N implies g in A ) by GROUP_2:125; :: thesis: verum