set g = Rev f;
Rev f is being_S-Seq

proof

thus Rev f is one-to-one ; :: according to TOPREAL1:def 10 :: thesis: ( 2 <= len (Rev f) & Rev f is unfolded & Rev f is s.n.c. & Rev f is special )
len (Rev f) = len f by FINSEQ_5:def 3;
hence len (Rev f) >= 2 by TOPREAL1:def 10; :: thesis: ( Rev f is unfolded & Rev f is s.n.c. & Rev f is special )
thus ( Rev f is unfolded & Rev f is s.n.c. & Rev f is special ) by Th29, Th36, Th42; :: thesis: verum

end;

hence for b₁ being FinSequence of (TOP-REAL 2) st b₁ = Rev f holds
b₁ is being_S-Seq ; :: thesis: verum