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

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

hence
f = g
; :: thesis: verumlet 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;thus f . s = H . (s,t) by A2

.= g . s by A3 ; :: thesis: verum