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

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