:: deftheorem Def3 defines REAL CHAIN_1:def 3 :
for n being Nat
for b₂ being FinSequenceSet of REAL holds
( b₂ = REAL n iff for x being object holds
( x in b₂ iff x is Function of (Seg n),REAL ) );