let G be Group; :: thesis: for N being normal Subgroup of G

for x being Element of G holds (x * N) * (x ") c= carr N

let N be normal Subgroup of G; :: thesis: for x being Element of G holds (x * N) * (x ") c= carr N

let x be Element of G; :: thesis: (x * N) * (x ") c= carr N

x * N c= N * x by GROUP_3:118;

then A1: (x * N) * (x ") c= (N * x) * (x ") by GROUP_3:5;

(N * x) * (x ") = N * (x * (x ")) by GROUP_2:107

.= N * (1_ G) by GROUP_1:def 5 ;

hence (x * N) * (x ") c= carr N by A1, GROUP_2:109; :: thesis: verum

for x being Element of G holds (x * N) * (x ") c= carr N

let N be normal Subgroup of G; :: thesis: for x being Element of G holds (x * N) * (x ") c= carr N

let x be Element of G; :: thesis: (x * N) * (x ") c= carr N

x * N c= N * x by GROUP_3:118;

then A1: (x * N) * (x ") c= (N * x) * (x ") by GROUP_3:5;

(N * x) * (x ") = N * (x * (x ")) by GROUP_2:107

.= N * (1_ G) by GROUP_1:def 5 ;

hence (x * N) * (x ") c= carr N by A1, GROUP_2:109; :: thesis: verum