:: deftheorem defines - SEQFUNC:def 6 :
for D being non empty set
for G, H being Functional_Sequence of D,REAL holds G - H = G + (- H);