for C being non empty set
for V being non empty vector-distributive RLSStruct
for f1, f2 being PartFunc of C,V
for f3 being Function of C,REAL holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)