for n, m being non zero Element of NAT
for R being RestFunc of (REAL-NS n)
for L being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds L * R is RestFunc of (REAL-NS m)