let r1, r2, x0, x1 be Real; 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; [!((r1 (#) f1) + (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) + (r2 * [!f2,x0,x1!])
[!((r1 (#) f1) + (r2 (#) f2)),x0,x1!] =
[!(r1 (#) f1),x0,x1!] + [!(r2 (#) f2),x0,x1!]
by Th32
.=
(r1 * [!f1,x0,x1!]) + [!(r2 (#) f2),x0,x1!]
by Th31
.=
(r1 * [!f1,x0,x1!]) + (r2 * [!f2,x0,x1!])
by Th31
;
hence
[!((r1 (#) f1) + (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) + (r2 * [!f2,x0,x1!])
; verum