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