theorem FTh41: :: ORDEQ_02:4

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