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