let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is being_S-Seq implies ( f is one-to-one & f is unfolded & f is s.n.c. & f is special & not f is trivial ) )
assume A4: f is being_S-Seq ; :: thesis: ( f is one-to-one & f is unfolded & f is s.n.c. & f is special & not f is trivial )
then len f >= 2 by TOPREAL1:def 8;
hence ( f is one-to-one & f is unfolded & f is s.n.c. & f is special & not f is trivial ) by A4, NAT_D:60, TOPREAL1:def 8; :: thesis: verum