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

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