theorem Th31: :: SEQFUNC:32

for D being non empty set
for H being Functional_Sequence of D,REAL
for x being Element of D holds
( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) ) by Th28;