let f, g be Function of T,Y; :: thesis: ( ( for t being Point of T holds f . t = H . s,t ) & ( for t being Point of T holds g . t = H . s,t ) implies f = g )
assume that
A2: for t being Point of T holds f . t = H . s,t and
A3: for t being Point of T holds g . t = H . s,t ; :: thesis: f = g

now

let t be Point of T; :: thesis: f . t = g . t
thus f . t = H . s,t by A2
.= g . t by A3 ; :: thesis: verum

end;

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