theorem Th5: :: PDIFF_1:5

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