let n1, n2 be Homomorphism of G,(G ./. N); :: thesis: ( ( for a being Element of G holds n1 . a = a * N ) & ( for a being Element of G holds n2 . a = a * N ) implies n1 = n2 )
assume that
A10: for a being Element of G holds n1 . a = a * N and
A11: for a being Element of G holds n2 . a = a * N ; :: thesis: n1 = n2

now

let a be Element of G; :: thesis: n1 . a = n2 . a
( n1 . a = a * N & n2 . a = a * N ) by A10, A11;
hence n1 . a = n2 . a ; :: thesis: verum

end;

hence n1 = n2 by FUNCT_2:113; :: thesis: verum