let G be Group; :: thesis: for x, y being Element of G
for N being normal Subgroup of G st y in N holds
(x * y) * (x ") in N
let x, y be Element of G; :: thesis: for N being normal Subgroup of G st y in N holds
(x * y) * (x ") in N
let N be normal Subgroup of G; :: thesis: ( y in N implies (x * y) * (x ") in N )
assume y in N ; :: thesis: (x * y) * (x ") in N
then x * y in x * N by GROUP_2:125;
then x * y in N * x by GROUP_3:140;
then consider y1 being Element of G such that
A3: ( x * y = y1 * x & y1 in N ) by GROUP_2:126;
(x * y) * (x ") = y1 * (x * (x ")) by A3, GROUP_1:def 4
.= y1 * (1_ G) by GROUP_1:def 6
.= y1 by GROUP_1:def 5 ;
hence (x * y) * (x ") in N by A3; :: thesis: verum