let p1, p2 be Homomorphism of (product F),(F . i); :: thesis: ( ( for h being Element of (product F) holds p1 . h = h . i ) & ( for h being Element of (product F) holds p2 . h = h . i ) implies p1 = p2 )
assume A1: for h being Element of (product F) holds p1 . h = h . i ; :: thesis: ( ex h being Element of (product F) st not p2 . h = h . i or p1 = p2 )
assume A2: for h being Element of (product F) holds p2 . h = h . i ; :: thesis: p1 = p2
for x being Element of (product F) holds p1 . x = p2 . x

proof

let x be Element of (product F); :: thesis: p1 . x = p2 . x
p1 . x = x . i by A1;
hence p1 . x = p2 . x by A2; :: thesis: verum

end;

hence p1 = p2 by FUNCT_2:def 8; :: thesis: verum