theorem :: CFUNCT_1:20

for C being non empty set
for f1, f2, f3 being PartFunc of C,COMPLEX holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) by Th19;