:: deftheorem Def4 defines ||. SEQFUNC2:def 3 :
for D being non empty set
for Y being non empty NORMSTR
for H being Functional_Sequence of D, the carrier of Y
for b₄ being Functional_Sequence of D,REAL holds
( b₄ = ||.H.|| iff for n being Nat holds b₄ . n = ||.(H . n).|| );