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