reconsider H = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by Lm6;
let IT1, IT2 be Homomorphism of G,(G ./. N); :: thesis: ( ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
IT1 = nat_hom H ) & ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
IT2 = nat_hom H ) implies IT1 = IT2 )
assume for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
IT1 = nat_hom H ; :: thesis: ( ex H being strict normal Subgroup of G st
( H = multMagma(# the carrier of N, the multF of N #) & not IT2 = nat_hom H ) or IT1 = IT2 )
then A16: IT1 = nat_hom H ;
assume for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
IT2 = nat_hom H ; :: thesis: IT1 = IT2
hence IT1 = IT2 by A16; :: thesis: verum