for n, m being non zero Element of NAT
for R1 being RestFunc of (REAL-NS n) st R1 /. 0 = 0. (REAL-NS n) holds
for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds
for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m)