let O be set ; :: thesis: for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds nat_hom N is onto
let G be GroupWithOperators of O; :: thesis: for N being normal StableSubgroup of G holds nat_hom N is onto
let N be normal StableSubgroup of G; :: thesis: nat_hom N is onto
Image (nat_hom N) = G ./. N by Th50;
hence nat_hom N is onto by Th51; :: thesis: verum