theorem :: VALUED_1:15

for C being set
for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2
for c being Element of C holds (f1 - f2) . c = (f1 . c) - (f2 . c)