let G, H be strict Group; :: thesis: for h being Homomorphism of G,H
for A being strict normal Subgroup of G holds h .: A is strict normal Subgroup of Image h
let h be Homomorphism of G,H; :: thesis: for A being strict normal Subgroup of G holds h .: A is strict normal Subgroup of Image h
let A be strict normal Subgroup of G; :: thesis: h .: A is strict normal Subgroup of Image h
reconsider C = h .: A as strict Subgroup of Image h by GRSOLV_1:9;
for b being Element of (Image h) holds b * C c= C * b

proof

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

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

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

end;

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

end;

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