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

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