theorem Th3: :: SEQFUNC:3

for D being non empty set
for G, H, H1 being Functional_Sequence of D,REAL holds
( H1 = G - H iff for n being Nat holds H1 . n = (G . n) - (H . n) )