theorem Th41: :: NDIFF_4:41

for n being non zero Element of NAT
for J being Function of (REAL-NS 1),REAL st J = proj (1,1) holds
( ( for R being RestFunc of (REAL-NS n) holds R * J is RestFunc of (REAL-NS 1),(REAL-NS n) ) & ( for L being LinearFunc of (REAL-NS n) holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) ) )