let f be FinSequence of (TOP-REAL 2); :: thesis: ( len f >= 2 implies rng f c= L~ f )
assume A1: len f >= 2 ; :: thesis: rng f c= L~ f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in L~ f )
assume x in rng f ; :: thesis: x in L~ f
then consider i being Element of NAT such that
A2: i in dom f and
A3: f /. i = x by PARTFUN2:2;
A4: 1 <= i by A2, FINSEQ_3:25;
A5: i <= len f by A2, FINSEQ_3:25;
A6: f /. i in LSeg ((f /. i),(f /. (i + 1))) by RLTOPSP1:68;

per cases ( i = len f or i <> len f ) ;

suppose A7: i = len f ; :: thesis: x in L~ f

then consider j being Nat such that
A8: j + 1 = i by A1, NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
1 + 1 <= j + 1 by A1, A7, A8;
then A9: 1 <= j by XREAL_1:6;
f /. (j + 1) in LSeg ((f /. j),(f /. (j + 1))) by RLTOPSP1:68;
hence x in L~ f by A3, A7, A8, A9, Th15; :: thesis: verum

end;

suppose i <> len f ; :: thesis: x in L~ f

then i < len f by A5, XXREAL_0:1;
then i + 1 <= len f by NAT_1:13;
hence x in L~ f by A3, A4, A6, Th15; :: thesis: verum

end;

end;