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 :: thesis: for S being Element of (G ./. N) holds S in Image (nat_hom N)

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 Th13;
(nat_hom N) . a = a * N by Def8;
hence S in Image (nat_hom N) by A1, Th45; :: thesis: verum

end;

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