:: deftheorem Def3 defines - SEQFUNC:def 3 :
for D being non empty set
for H, b₃ being Functional_Sequence of D,REAL holds
( b₃ = - H iff for n being Nat holds b₃ . n = - (H . n) );