theorem :: CFUNCT_1:16

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