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

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

hence
F1 = F2
by FUNCT_2:63; :: thesis: verumlet 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;thus F1 . x = (1_ (product F)) +* (i,x) by A1

.= F2 . x by A2 ; :: thesis: verum