let G be Group; :: thesis: for N being normal Subgroup of G holds nat_hom N is onto
let N be normal Subgroup of G; :: thesis: nat_hom N is onto
Image (nat_hom N) = G ./. N by Th48;
hence nat_hom N is onto by Th57; :: thesis: verum