let g, h be Homomorphism of G,H; :: thesis: ( ( for a being Element of G holds g . a = 1_ H ) & ( for a being Element of G holds h . a = 1_ H ) implies g = h )
assume that
A1: for a being Element of G holds g . a = 1_ H and
A2: for a being Element of G holds h . a = 1_ H ; :: thesis: g = h
for a being Element of G holds g . a = h . a

proof

let a be Element of G; :: thesis: g . a = h . a
g . a = 1_ H by A1;
hence g . a = h . a by A2; :: thesis: verum

end;

hence g = h by FUNCT_2:113; :: thesis: verum