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

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

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

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