deffunc H₁( Element of 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();
take f ; :: thesis: f is linear
thus f is linear by Def2, A1; :: thesis: verum