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