:: deftheorem defines - SEQFUNC2:def 5 :
for D being non empty set
for Y being RealNormSpace
for G, H being Functional_Sequence of D, the carrier of Y holds G - H = G + (- H);