theorem Th6: :: PDIFF_1:6

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 holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) )