theorem :: DIFF_3:30

for r1, r2, x0, x1 being Real
for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) - (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) - (r2 * [!f2,x0,x1!])