theorem :: SEQFUNC:2

for D being non empty set
for G, H, H1 being Functional_Sequence of D,REAL holds
( H1 = G / H iff for n being Nat holds H1 . n = (G . n) / (H . n) )