let r1, r2, x0, x1 be Real; :: thesis: for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) - (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) - (r2 * [!f2,x0,x1!])
let f1, f2 be Function of REAL,REAL; :: thesis: [!((r1 (#) f1) - (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) - (r2 * [!f2,x0,x1!])
set g1 = r1 (#) f1;
set g2 = r2 (#) f2;
[!((r1 (#) f1) - (r2 (#) f2)),x0,x1!] = [!(r1 (#) f1),x0,x1!] - [!(r2 (#) f2),x0,x1!] by Th25
.= (r1 * [!f1,x0,x1!]) - [!(r2 (#) f2),x0,x1!] by DIFF_1:31
.= (r1 * [!f1,x0,x1!]) - (r2 * [!f2,x0,x1!]) by DIFF_1:31 ;
hence [!((r1 (#) f1) - (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) - (r2 * [!f2,x0,x1!]) ; :: thesis: verum