for Y being RealNormSpace
for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds
( ( for R being RestFunc of (REAL-NS 1),Y holds R * I is RestFunc of Y ) & ( for L being LinearOperator of (REAL-NS 1),Y holds L * I is LinearFunc of Y ) )