:: deftheorem Def6 defines |. TOPRNS_1:def 6 :
for N being Nat
for seq being Real_Sequence of N
for b₃ being Real_Sequence holds
( b₃ = |.seq.| iff for n being Nat holds b₃ . n = |.(seq . n).| );