deffunc H₁( Point of T) -> Element of the carrier of Y = H . [s,$1];
consider f being Function of the carrier of T, the carrier of Y such that
A1: for x being Element of T holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for t being Point of T holds f . t = H . (s,t)
let x be Point of T; :: thesis: f . x = H . (s,x)
thus f . x = H . (s,x) by A1; :: thesis: verum