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

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