let h1, h2 be Function of (Hom (R,M,N)),(Hom (R,M1,N)); :: thesis: ( ( for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & h1 . f = f1 * u ) ) & ( for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & h2 . f = f1 * u ) ) implies h1 = h2 )
assume that
A3: for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & h1 . f = f1 * u ) and
A4: for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & h2 . f = f1 * u ) ; :: thesis: h1 = h2

now :: thesis: for y being Element of (Hom (R,M,N)) holds h1 . y = h2 . y

let y be Element of (Hom (R,M,N)); :: thesis: h1 . y = h2 . y
consider f1 being Homomorphism of R,M,N such that
A5: ( y = f1 & h1 . y = f1 * u ) by A3;
consider f2 being Homomorphism of R,M,N such that
A6: ( y = f2 & h2 . y = f2 * u ) by A4;
thus h1 . y = h2 . y by A5, A6; :: thesis: verum

end;

hence h1 = h2 ; :: thesis: verum