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

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