let G be Group; :: thesis: for x being set
for N being normal Subgroup of G holds
( x in G ./. N iff ex a being Element of G st
( x = a * N & x = N * a ) )
let x be set ; :: thesis: for N being normal Subgroup of G holds
( x in G ./. N iff ex a being Element of G st
( x = a * N & x = N * a ) )
let N be normal Subgroup of G; :: thesis: ( x in G ./. N iff ex a being Element of G st
( x = a * N & x = N * a ) )
thus ( x in G ./. N implies ex a being Element of G st
( x = a * N & x = N * a ) ) :: thesis: ( ex a being Element of G st
( x = a * N & x = N * a ) implies x in G ./. N )

proof

assume x in G ./. N ; :: thesis: ex a being Element of G st
( x = a * N & x = N * a )
then x is Element of (G ./. N) by STRUCT_0:def 5;
hence ex a being Element of G st
( x = a * N & x = N * a ) by Th15; :: thesis: verum

end;

given a being Element of G such that A1: ( x = a * N & x = N * a ) ; :: thesis: x in G ./. N
x is Element of (G ./. N) by A1, Th16;
hence x in G ./. N by STRUCT_0:def 5; :: thesis: verum