for X, Y, W being RealNormSpace
for I being Function of X,Y
for f1, f2 being PartFunc of Y,W holds
( (f1 + f2) * I = (f1 * I) + (f2 * I) & (f1 - f2) * I = (f1 * I) - (f2 * I) )