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
A12: for a being Element of G holds n1 . a = a * N and
A13: 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 by A12;
hence n1 . a = n2 . a by A13; :: thesis: verum
end;
hence n1 = n2 by FUNCT_2:113; :: thesis: verum