theorem Th7: :: FDIFF_1:7

for R being RestFunc
for L being LinearFunc holds
( R (#) L is RestFunc & L (#) R is RestFunc )