let f be FinSequence of (TOP-REAL 2); :: thesis: for n being Element of NAT st 2 <= n & f is being_S-Seq holds
f | n is being_S-Seq
let n be Element of NAT ; :: thesis: ( 2 <= n & f is being_S-Seq implies f | n is being_S-Seq )
assume that
A1: 2 <= n and
A2: f is being_S-Seq ; :: thesis: f | n is being_S-Seq
A3: len f >= 2 by A2, TOPREAL1:def 8;
A4: now :: thesis: ( ( n <= len f & len (f | n) >= 2 ) or ( n > len f & len (f | n) >= 2 ) )
per cases ( n <= len f or n > len f ) ;
case n <= len f ; :: thesis: len (f | n) >= 2
hence len (f | n) >= 2 by A1, FINSEQ_1:59; :: thesis: verum
end;
case n > len f ; :: thesis: len (f | n) >= 2
hence len (f | n) >= 2 by A3, FINSEQ_1:58; :: thesis: verum
end;
end;
end;
reconsider f9 = f as one-to-one special unfolded s.n.c. FinSequence of (TOP-REAL 2) by A2;
f9 | n is one-to-one ;
hence f | n is being_S-Seq by A4, TOPREAL1:def 8; :: thesis: verum