:: deftheorem Def2 defines " SEQFUNC:def 2 :
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) ^ );