let G be Group; :: thesis: for N being Subgroup of G st ( for x, y being Element of G st y in N holds

(x * y) * (x ") in N ) holds

N is normal

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

(x * y) * (x ") in N ) implies N is normal )

assume A1: for x, y being Element of G st y in N holds

(x * y) * (x ") in N ; :: thesis: N is normal

for x being Element of G holds x * N c= N * x

(x * y) * (x ") in N ) holds

N is normal

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

(x * y) * (x ") in N ) implies N is normal )

assume A1: for x, y being Element of G st y in N holds

(x * y) * (x ") in N ; :: thesis: N is normal

for x being Element of G holds x * N c= N * x

proof

hence
N is normal
by GROUP_3:118; :: thesis: verum
let x be Element of G; :: thesis: x * N c= N * x

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x * N or z in N * x )

assume A2: z in x * N ; :: thesis: z in N * x

then reconsider z = z as Element of G ;

consider z1 being Element of G such that

A3: ( z = x * z1 & z1 in N ) by A2, GROUP_2:103;

A4: (x * z1) * (x ") in N by A1, A3;

((x * z1) * (x ")) * x = z by A3, GROUP_3:1;

hence z in N * x by A4, GROUP_2:104; :: thesis: verum

end;let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x * N or z in N * x )

assume A2: z in x * N ; :: thesis: z in N * x

then reconsider z = z as Element of G ;

consider z1 being Element of G such that

A3: ( z = x * z1 & z1 in N ) by A2, GROUP_2:103;

A4: (x * z1) * (x ") in N by A1, A3;

((x * z1) * (x ")) * x = z by A3, GROUP_3:1;

hence z in N * x by A4, GROUP_2:104; :: thesis: verum