theorem :: SEQFUNC:9

for D being non empty set
for r being Real
for G, H being Functional_Sequence of D,REAL holds
( r (#) (G + H) = (r (#) G) + (r (#) H) & r (#) (G - H) = (r (#) G) - (r (#) H) )