let n be Element of NAT ; for h, r, x being Real
for f1, f2 being Function of REAL,REAL holds ((fdif (((r (#) f1) + f2),h)) . (n + 1)) . x = (r * (((fdif (f1,h)) . (n + 1)) . x)) + (((fdif (f2,h)) . (n + 1)) . x)
let h, r, x be Real; for f1, f2 being Function of REAL,REAL holds ((fdif (((r (#) f1) + f2),h)) . (n + 1)) . x = (r * (((fdif (f1,h)) . (n + 1)) . x)) + (((fdif (f2,h)) . (n + 1)) . x)
let f1, f2 be Function of REAL,REAL; ((fdif (((r (#) f1) + f2),h)) . (n + 1)) . x = (r * (((fdif (f1,h)) . (n + 1)) . x)) + (((fdif (f2,h)) . (n + 1)) . x)
set g = r (#) f1;
((fdif (((r (#) f1) + f2),h)) . (n + 1)) . x =
(((fdif ((r (#) f1),h)) . (n + 1)) . x) + (((fdif (f2,h)) . (n + 1)) . x)
by DIFF_1:8
.=
(r * (((fdif (f1,h)) . (n + 1)) . x)) + (((fdif (f2,h)) . (n + 1)) . x)
by DIFF_1:7
;
hence
((fdif (((r (#) f1) + f2),h)) . (n + 1)) . x = (r * (((fdif (f1,h)) . (n + 1)) . x)) + (((fdif (f2,h)) . (n + 1)) . x)
; verum