set g = Rev f;

Rev f is being_S-Seq_{1} being FinSequence of (TOP-REAL 2) st b_{1} = Rev f holds

b_{1} is being_S-Seq
; :: thesis: verum

Rev f is being_S-Seq

proof

hence
for b
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;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

b