let G be Group; :: thesis: for N being normal Subgroup of G
for g1, g2 being Element of G st g1 * N = g2 * N holds
ex n being Element of G st
( n in N & g1 = g2 * n )
let N be normal Subgroup of G; :: thesis: for g1, g2 being Element of G st g1 * N = g2 * N holds
ex n being Element of G st
( n in N & g1 = g2 * n )
let g1, g2 be Element of G; :: thesis: ( g1 * N = g2 * N implies ex n being Element of G st
( n in N & g1 = g2 * n ) )
assume A1: g1 * N = g2 * N ; :: thesis: ex n being Element of G st
( n in N & g1 = g2 * n )
consider n being Element of G such that
A2: n = (g2 ") * g1 ;
take n ; :: thesis: ( n in N & g1 = g2 * n )
thus n in N by A1, A2, GROUP_2:114; :: thesis: g1 = g2 * n
thus g2 * n = (g2 * (g2 ")) * g1 by A2, GROUP_1:def 3
.= (1_ G) * g1 by GROUP_1:def 5
.= g1 by GROUP_1:def 4 ; :: thesis: verum