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

for x, y being Element of G st y in H holds

( (x * y) * (x ") in H & x * (y * (x ")) in H )

let H be normal Subgroup of G; :: thesis: for x, y being Element of G st y in H holds

( (x * y) * (x ") in H & x * (y * (x ")) in H )

let x, y be Element of G; :: thesis: ( y in H implies ( (x * y) * (x ") in H & x * (y * (x ")) in H ) )

assume A1: y in H ; :: thesis: ( (x * y) * (x ") in H & x * (y * (x ")) in H )

x * H = H * x by GROUP_3:117;

then consider g being Element of G such that

A2: ( x * y = g * x & g in H ) by A1, GROUP_2:103, GROUP_2:104;

(x * y) * (x ") = g by A2, GROUP_3:1;

hence ( (x * y) * (x ") in H & x * (y * (x ")) in H ) by A2, GROUP_1:def 3; :: thesis: verum

for x, y being Element of G st y in H holds

( (x * y) * (x ") in H & x * (y * (x ")) in H )

let H be normal Subgroup of G; :: thesis: for x, y being Element of G st y in H holds

( (x * y) * (x ") in H & x * (y * (x ")) in H )

let x, y be Element of G; :: thesis: ( y in H implies ( (x * y) * (x ") in H & x * (y * (x ")) in H ) )

assume A1: y in H ; :: thesis: ( (x * y) * (x ") in H & x * (y * (x ")) in H )

x * H = H * x by GROUP_3:117;

then consider g being Element of G such that

A2: ( x * y = g * x & g in H ) by A1, GROUP_2:103, GROUP_2:104;

(x * y) * (x ") = g by A2, GROUP_3:1;

hence ( (x * y) * (x ") in H & x * (y * (x ")) in H ) by A2, GROUP_1:def 3; :: thesis: verum