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 )

hence ( A = g * N implies g in A ) by GROUP_2:103; :: thesis: verum

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 )

( g = g * (1_ G) & 1_ G in N )
by GROUP_1:def 4, GROUP_2:46;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;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

hence ( A = g * N implies g in A ) by GROUP_2:103; :: thesis: verum