theorem :: SEQFUNC:17

for D being non empty set
for G, H being Functional_Sequence of D,REAL holds abs (G / H) = (abs G) / (abs H)