theorem Th10: :: FIB_NUM:10

for f, g being Real_Sequence
for n being Nat holds
( (f /" g) . n = (f . n) / (g . n) & (f /" g) . n = (f . n) * ((g . n) ") )