deffunc H_{1}( Point of S) -> Element of the carrier of Y = H . [$1,t];

consider f being Function of the carrier of S, the carrier of Y such that

A1: for x being Element of S holds f . x = H_{1}(x)
from FUNCT_2:sch 4();

take f ; :: thesis: for s being Point of S holds f . s = H . (s,t)

let x be Point of S; :: thesis: f . x = H . (x,t)

thus f . x = H . (x,t) by A1; :: thesis: verum

consider f being Function of the carrier of S, the carrier of Y such that

A1: for x being Element of S holds f . x = H

take f ; :: thesis: for s being Point of S holds f . s = H . (s,t)

let x be Point of S; :: thesis: f . x = H . (x,t)

thus f . x = H . (x,t) by A1; :: thesis: verum