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 A11: 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 )
assume A12: 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
reconsider H = multMagma(# the carrier of N,the multF of N #) as strict normal Subgroup of G by Lm7;
( IT1 = nat_hom H & IT2 = nat_hom H ) by A11, A12;
hence IT1 = IT2 ; :: thesis: verum