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;

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 )
;

end;

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;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