:: deftheorem Def3 defines Rev FINSEQ_5:def 3 :
for f, b₂ being FinSequence holds
( b₂ = Rev f iff ( len b₂ = len f & ( for i being Nat st i in dom b₂ holds
b₂ . i = f . (((len f) - i) + 1) ) ) );