let G, H be strict Group; :: thesis: for h being Homomorphism of G,H
for A, B being strict Subgroup of G st A is strict normal Subgroup of B holds
h .: A is strict normal Subgroup of h .: B
let h be Homomorphism of G,H; :: thesis: for A, B being strict Subgroup of G st A is strict normal Subgroup of B holds
h .: A is strict normal Subgroup of h .: B
let A, B be strict Subgroup of G; :: thesis: ( A is strict normal Subgroup of B implies h .: A is strict normal Subgroup of h .: B )
assume A is strict normal Subgroup of B ; :: thesis: h .: A is strict normal Subgroup of h .: B
then reconsider A1 = A as strict normal Subgroup of B ;
reconsider C = h .: A1 as strict Subgroup of h .: B by Th12;
for b2 being Element of (h .: B) holds b2 * C c= C * b2

proof

let b2 be Element of (h .: B); :: thesis: b2 * C c= C * b2
A1: b2 in h .: B by STRUCT_0:def 5;

now :: thesis: for x being object st x in b2 * C holds
x in C * b2

consider b1 being Element of B such that
A2: b2 = (h | B) . b1 by A1, GROUP_6:45;
reconsider b1 = b1 as Element of G by GROUP_2:42;
A3: b2 = h . b1 by A2, FUNCT_1:49;
reconsider b = b1 as Element of B ;
let x be object ; :: thesis: ( x in b2 * C implies x in C * b2 )
assume x in b2 * C ; :: thesis: x in C * b2
then consider g being Element of (h .: B) such that
A4: x = b2 * g and
A5: g in C by GROUP_2:103;
consider g1 being Element of A1 such that
A6: g = (h | A1) . g1 by A5, GROUP_6:45;
reconsider g1 = g1 as Element of G by GROUP_2:42;
g = h . g1 by A6, FUNCT_1:49;
then A7: x = (h . b1) * (h . g1) by A3, A4, GROUP_2:43
.= h . (b1 * g1) by GROUP_6:def 6 ;
g1 in A1 by STRUCT_0:def 5;
then A8: b1 * g1 in b1 * A1 by GROUP_2:103;
A9: h .: (A1 * b1) = (h .: A1) * (h . b1) by Th13;
b1 * A1 = b * A1 by GROUP_6:2
.= A1 * b by GROUP_3:117
.= A1 * b1 by GROUP_6:2 ;
then x in h .: (A1 * b1) by A7, A8, FUNCT_2:35;
hence x in C * b2 by A3, A9, GROUP_6:2; :: thesis: verum

end;

hence b2 * C c= C * b2 ; :: thesis: verum

end;

hence h .: A is strict normal Subgroup of h .: B by GROUP_3:118; :: thesis: verum