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