theorem :: DIFF_3:28

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