deffunc H₁( Real) -> Element of the carrier of F = F * (0. F);
consider f being Function of REAL, the carrier of F such that
A1: for x being Element of REAL holds f . x = H₁(x) from FUNCT_2:sch 4();
A2: for x being Real holds f /. x = H₁(x)

proof

let x be Real; :: thesis: f /. x = H₁(x)
reconsider x = x as Element of REAL by XREAL_0:def 1;
f /. x = H₁(x) by A1;
hence f /. x = H₁(x) ; :: thesis: verum

end;

take f ; :: thesis: f is linear
thus f is linear by A2; :: thesis: verum