let n be Element of NAT ; :: thesis: for r1, r2, h, x being Real
for f1, f2 being Function of REAL ,REAL holds ((cdif ((r1 (#) f1) + (r2 (#) f2)),h) . (n + 1)) . x = (r1 * (((cdif f1,h) . (n + 1)) . x)) + (r2 * (((cdif f2,h) . (n + 1)) . x))
let r1, r2, h, x be Real; :: thesis: for f1, f2 being Function of REAL ,REAL holds ((cdif ((r1 (#) f1) + (r2 (#) f2)),h) . (n + 1)) . x = (r1 * (((cdif f1,h) . (n + 1)) . x)) + (r2 * (((cdif f2,h) . (n + 1)) . x))
let f1, f2 be Function of REAL ,REAL ; :: thesis: ((cdif ((r1 (#) f1) + (r2 (#) f2)),h) . (n + 1)) . x = (r1 * (((cdif f1,h) . (n + 1)) . x)) + (r2 * (((cdif f2,h) . (n + 1)) . x))
set g1 = r1 (#) f1;
set g2 = r2 (#) f2;
((cdif ((r1 (#) f1) + (r2 (#) f2)),h) . (n + 1)) . x = (((cdif (r1 (#) f1),h) . (n + 1)) . x) + (((cdif (r2 (#) f2),h) . (n + 1)) . x) by Th22
.= (r1 * (((cdif f1,h) . (n + 1)) . x)) + (((cdif (r2 (#) f2),h) . (n + 1)) . x) by Th21
.= (r1 * (((cdif f1,h) . (n + 1)) . x)) + (r2 * (((cdif f2,h) . (n + 1)) . x)) by Th21 ;
hence ((cdif ((r1 (#) f1) + (r2 (#) f2)),h) . (n + 1)) . x = (r1 * (((cdif f1,h) . (n + 1)) . x)) + (r2 * (((cdif f2,h) . (n + 1)) . x)) ; :: thesis: verum