theorem Th15: :: SEQFUNC:16

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