:: deftheorem Def1 defines Rev AFINSQ_2:def 1 :
for p, b₂ being XFinSequence holds
( b₂ = Rev p iff ( len b₂ = len p & ( for i being Nat st i in dom b₂ holds
b₂ . i = p . ((len p) - (i + 1)) ) ) );