let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Nat st i in dom f & 2 <= len f holds
f /. i in L~ f
let i be Nat; :: thesis: ( i in dom f & 2 <= len f implies f /. i in L~ f )
assume that
A1: i in dom f and
A2: 2 <= len f ; :: thesis: f /. i in L~ f
A3: 1 <= i by A1, FINSEQ_3:25;
A4: i <= len f by A1, FINSEQ_3:25;

per cases ( i = len f or i < len f ) by A4, XXREAL_0:1;

suppose A5: i = len f ; :: thesis: f /. i in L~ f

reconsider l = i - 1 as Element of NAT by A3, INT_1:5;
1 + 1 <= i by A2, A5;
then 1 <= l by XREAL_1:19;
then A6: f /. (l + 1) in LSeg (f,l) by A4, TOPREAL1:21;
LSeg (f,l) c= L~ f by TOPREAL3:19;
hence f /. i in L~ f by A6; :: thesis: verum

end;

suppose i < len f ; :: thesis: f /. i in L~ f

then i + 1 <= len f by NAT_1:13;
then A7: f /. i in LSeg (f,i) by A3, TOPREAL1:21;
LSeg (f,i) c= L~ f by TOPREAL3:19;
hence f /. i in L~ f by A7; :: thesis: verum

end;

end;