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 Lm6;
reconsider H = G ./. N as strict StableSubgroup of G ./. N by Lm3;
A1: G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) by Lm34;
the carrier of (Image (nat_hom N)) = (nat_hom N) .: the carrier of G by Def22
.= (nat_hom N9) .: the carrier of G by Def20
.= the carrier of (Image (nat_hom N9)) by GROUP_6:def 10
.= the carrier of H by A1, GROUP_6:48 ;
hence Image (nat_hom N) = G ./. N by Lm4; :: thesis: verum