set g = Rev f;
Rev f is being_S-Seq
proof
thus Rev f is one-to-one ; :: according to TOPREAL1:def 8 :: 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 8; :: 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 Th28, Th35, Th40; :: thesis: verum
end;
hence for b1 being FinSequence of (TOP-REAL 2) st b1 = Rev f holds
b1 is being_S-Seq ; :: thesis: verum