let G be Group; :: thesis: for x being object
for N being normal Subgroup of G st x in Cosets N holds
ex a being Element of G st
( x = a * N & x = N * a )
let x be object ; :: thesis: for N being normal Subgroup of G st x in Cosets N holds
ex a being Element of G st
( x = a * N & x = N * a )
let N be normal Subgroup of G; :: thesis: ( x in Cosets N implies ex a being Element of G st
( x = a * N & x = N * a ) )
assume x in Cosets N ; :: thesis: ex a being Element of G st
( x = a * N & x = N * a )
then consider a being Element of G such that
A1: x = a * N by GROUP_2:def 15;
x = N * a by A1, GROUP_3:117;
hence ex a being Element of G st
( x = a * N & x = N * a ) by A1; :: thesis: verum