theorem :: SEQFUNC:18

for D being non empty set
for r being Real
for H being Functional_Sequence of D,REAL holds abs (r (#) H) = |.r.| (#) (abs H)