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 :: thesis: for s being Point of S holds f . s = g . s

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 ; :: thesis: verum