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