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:103;
then x * y in N * x by GROUP_3:117;
then consider y1 being Element of G such that
A1: ( x * y = y1 * x & y1 in N ) by GROUP_2:104;
(x * y) * (x ") = y1 * (x * (x ")) by A1, GROUP_1:def 3
.= y1 * (1_ G) by GROUP_1:def 5
.= y1 by GROUP_1:def 4 ;
hence (x * y) * (x ") in N by A1; :: thesis: verum