let r, x0, x1 be Real; :: thesis: for f1, f2 being Function of REAL,REAL holds [!((r (#) f1) + f2),x0,x1!] = (r * [!f1,x0,x1!]) + [!f2,x0,x1!]
let f1, f2 be Function of REAL,REAL; :: thesis: [!((r (#) f1) + f2),x0,x1!] = (r * [!f1,x0,x1!]) + [!f2,x0,x1!]
set g = r (#) f1;
[!((r (#) f1) + f2),x0,x1!] = [!(r (#) f1),x0,x1!] + [!f2,x0,x1!] by DIFF_1:32
.= (r * [!f1,x0,x1!]) + [!f2,x0,x1!] by DIFF_1:31 ;
hence [!((r (#) f1) + f2),x0,x1!] = (r * [!f1,x0,x1!]) + [!f2,x0,x1!] ; :: thesis: verum