let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Element of NAT st i in dom f & 2 <= len f holds
f /. i in L~ f
let i be Element of 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:27;
A4: i <= len f by A1, FINSEQ_3:27;

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:18;
1 + 1 <= i by A2, A5;
then 1 <= l by XREAL_1:21;
then A6: f /. (l + 1) in LSeg f,l by A4, TOPREAL1:27;
LSeg f,l c= L~ f by TOPREAL3:26;
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:27;
LSeg f,i c= L~ f by TOPREAL3:26;
hence f /. i in L~ f by A7; :: thesis: verum

end;

end;