let r1, r2, x0, x1, x2, x3, x4 be Real; :: thesis: for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4!] = (r1 * [!f1,x0,x1,x2,x3,x4!]) + (r2 * [!f2,x0,x1,x2,x3,x4!])
let f1, f2 be Function of REAL,REAL; :: thesis: [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4!] = (r1 * [!f1,x0,x1,x2,x3,x4!]) + (r2 * [!f2,x0,x1,x2,x3,x4!])
[!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4!] = [!(r1 (#) f1),x0,x1,x2,x3,x4!] + [!(r2 (#) f2),x0,x1,x2,x3,x4!] by Th12
.= (r1 * [!f1,x0,x1,x2,x3,x4!]) + [!(r2 (#) f2),x0,x1,x2,x3,x4!] by Th11 ;
hence [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4!] = (r1 * [!f1,x0,x1,x2,x3,x4!]) + (r2 * [!f2,x0,x1,x2,x3,x4!]) by Th11; :: thesis: verum