for S, T being RealNormSpace
for R1 being RestFunc of S st R1 /. 0 = 0. S holds
for R2 being RestFunc of S,T st R2 /. (0. S) = 0. T holds
for L being LinearFunc of S holds R2 * (L + R1) is RestFunc of T