theorem Th9: :: FIB_NUM:9

for f, g, h being Real_Sequence st g is non-zero holds
(f /" g) (#) (g /" h) = f /" h