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