let F1, F2 be Homomorphism of (F . i),(ProjGroup (F,i)); :: thesis: ( ( for x being Element of (F . i) holds F1 . x = (1_ (product F)) +* (i,x) ) & ( for x being Element of (F . i) holds F2 . x = (1_ (product F)) +* (i,x) ) implies F1 = F2 )
assume that
A1: for x being Element of (F . i) holds F1 . x = (1_ (product F)) +* (i,x) and
A2: for x being Element of (F . i) holds F2 . x = (1_ (product F)) +* (i,x) ; :: thesis: F1 = F2

now :: thesis: for x being Element of (F . i) holds F1 . x = F2 . x

let x be Element of (F . i); :: thesis: F1 . x = F2 . x
thus F1 . x = (1_ (product F)) +* (i,x) by A1
.= F2 . x by A2 ; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:63; :: thesis: verum