reconsider a' = a, b' = b as Element of REAL by XREAL_0:def 1;
deffunc H₁( Real) -> Element of REAL = (a' * $1) + b';
consider f being Function of REAL , REAL such that
A1: for x being Element of REAL holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for x being real number holds f . x = (a * x) + b
let x be real number ; :: thesis: f . x = (a * x) + b
reconsider x' = x as Element of REAL by XREAL_0:def 1;
f . x' = (a' * x) + b' by A1;
hence f . x = (a * x) + b ; :: thesis: verum