deffunc H₁( Point of ) -> 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 holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for s being Point of holds f . s = H . s,t
let x be Point of ; :: thesis: f . x = H . x,t
thus f . x = H . x,t by A1; :: thesis: verum