let O be set ; :: thesis: for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds Image (nat_hom N) = G ./. N
let G be GroupWithOperators of O; :: thesis: for N being normal StableSubgroup of G holds Image (nat_hom N) = G ./. N
let N be normal StableSubgroup of G; :: thesis: Image (nat_hom N) = G ./. N
reconsider N9 = multMagma(# the carrier of N,the multF of N #) as strict normal Subgroup of G by Lm7;
reconsider H = G ./. N as strict StableSubgroup of G ./. N by Lm4;
A1: G ./. N9 = multMagma(# the carrier of (G ./. N),the multF of (G ./. N) #) by Lm35;
the carrier of (Image (nat_hom N)) = (nat_hom N) .: the carrier of G by Def25
.= (nat_hom N9) .: the carrier of G by Def23
.= the carrier of (Image (nat_hom N9)) by GROUP_6:def 11
.= the carrier of H by A1, GROUP_6:57 ;
hence Image (nat_hom N) = G ./. N by Lm5; :: thesis: verum