let n be Nat; for h, r1, r2, x being Real
for f1, f2 being Function of REAL,REAL holds ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((fdif (f1,h)) . (n + 1)) . x)) + (r2 * (((fdif (f2,h)) . (n + 1)) . x))
let h, r1, r2, x be Real; for f1, f2 being Function of REAL,REAL holds ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((fdif (f1,h)) . (n + 1)) . x)) + (r2 * (((fdif (f2,h)) . (n + 1)) . x))
let f1, f2 be Function of REAL,REAL; ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((fdif (f1,h)) . (n + 1)) . x)) + (r2 * (((fdif (f2,h)) . (n + 1)) . x))
set g1 = r1 (#) f1;
set g2 = r2 (#) f2;
((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x =
(((fdif ((r1 (#) f1),h)) . (n + 1)) . x) + (((fdif ((r2 (#) f2),h)) . (n + 1)) . x)
by Th8
.=
(r1 * (((fdif (f1,h)) . (n + 1)) . x)) + (((fdif ((r2 (#) f2),h)) . (n + 1)) . x)
by Th7
.=
(r1 * (((fdif (f1,h)) . (n + 1)) . x)) + (r2 * (((fdif (f2,h)) . (n + 1)) . x))
by Th7
;
hence
((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((fdif (f1,h)) . (n + 1)) . x)) + (r2 * (((fdif (f2,h)) . (n + 1)) . x))
; verum