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

now

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

end;

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