theorem Th40: :: NDIFF_4:40

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