for f1 being PartFunc of REAL,REAL
for n, m being Real holds (n (#) f1) + (m (#) f1) = (n + m) (#) f1