let G be strict Group; :: thesis: for H being Subgroup of G st H is normal holds

for a, b being Element of G st b is Element of H holds

b |^ a in H

let H be Subgroup of G; :: thesis: ( H is normal implies for a, b being Element of G st b is Element of H holds

b |^ a in H )

assume A1: H is normal ; :: thesis: for a, b being Element of G st b is Element of H holds

b |^ a in H

set A = carr H;

let a, b be Element of G; :: thesis: ( b is Element of H implies b |^ a in H )

H * a = a * H by A1, GROUP_3:117;

then ((a ") * H) * a = (a ") * (a * H) by GROUP_2:106;

then ((a ") * H) * a = ((a ") * a) * H by GROUP_2:105;

then ((a ") * H) * a = (1_ G) * H by GROUP_1:def 5;

then ((a ") * H) * a = carr H by GROUP_2:109;

then the carrier of (H |^ a) = carr H by GROUP_3:59;

then A2: (carr H) |^ a = carr H by GROUP_3:def 6;

assume b is Element of H ; :: thesis: b |^ a in H

then (a ") * b in (a ") * (carr H) by GROUP_2:27;

then ((a ") * b) * a in ((a ") * (carr H)) * a by GROUP_2:28;

then b |^ a in carr H by A2, GROUP_3:50;

hence b |^ a in H by STRUCT_0:def 5; :: thesis: verum

for a, b being Element of G st b is Element of H holds

b |^ a in H

let H be Subgroup of G; :: thesis: ( H is normal implies for a, b being Element of G st b is Element of H holds

b |^ a in H )

assume A1: H is normal ; :: thesis: for a, b being Element of G st b is Element of H holds

b |^ a in H

set A = carr H;

let a, b be Element of G; :: thesis: ( b is Element of H implies b |^ a in H )

H * a = a * H by A1, GROUP_3:117;

then ((a ") * H) * a = (a ") * (a * H) by GROUP_2:106;

then ((a ") * H) * a = ((a ") * a) * H by GROUP_2:105;

then ((a ") * H) * a = (1_ G) * H by GROUP_1:def 5;

then ((a ") * H) * a = carr H by GROUP_2:109;

then the carrier of (H |^ a) = carr H by GROUP_3:59;

then A2: (carr H) |^ a = carr H by GROUP_3:def 6;

assume b is Element of H ; :: thesis: b |^ a in H

then (a ") * b in (a ") * (carr H) by GROUP_2:27;

then ((a ") * b) * a in ((a ") * (carr H)) * a by GROUP_2:28;

then b |^ a in carr H by A2, GROUP_3:50;

hence b |^ a in H by STRUCT_0:def 5; :: thesis: verum