let G be Group; :: thesis: for N being normal Subgroup of G holds Image (nat_hom N) = G ./. N
let N be normal Subgroup of G; :: thesis: Image (nat_hom N) = G ./. N

now

let S be Element of (G ./. N); :: thesis: S in Image (nat_hom N)
consider a being Element of G such that
A1: S = a * N and
S = N * a by Th15;
(nat_hom N) . a = a * N by Def9;
hence S in Image (nat_hom N) by A1, Th54; :: thesis: verum

end;

hence Image (nat_hom N) = G ./. N by GROUP_2:71; :: thesis: verum