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