for m, n being non zero Nat
for i being Nat
for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds
( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) )