let f be non empty unfolded s.n.c. FinSequence of (TOP-REAL 2); for i being Nat st 1 <= i & i < len f holds
(LSeg (f,i)) /\ (rng f) = {(f /. i),(f /. (i + 1))}
let i be Nat; ( 1 <= i & i < len f implies (LSeg (f,i)) /\ (rng f) = {(f /. i),(f /. (i + 1))} )
assume that
A1:
1 <= i
and
A2:
i < len f
; (LSeg (f,i)) /\ (rng f) = {(f /. i),(f /. (i + 1))}
A3:
i in dom f
by A1, A2, FINSEQ_3:25;
then
f /. i = f . i
by PARTFUN1:def 6;
then A4:
f /. i in rng f
by A3, FUNCT_1:3;
assume A5:
(LSeg (f,i)) /\ (rng f) <> {(f /. i),(f /. (i + 1))}
; contradiction
A6:
i + 1 <= len f
by A2, NAT_1:13;
then
f /. i in LSeg (f,i)
by A1, TOPREAL1:21;
then A7:
f /. i in (LSeg (f,i)) /\ (rng f)
by A4, XBOOLE_0:def 4;
A8:
1 < i + 1
by A1, XREAL_1:29;
then A9:
i + 1 in dom f
by A6, FINSEQ_3:25;
then
f /. (i + 1) = f . (i + 1)
by PARTFUN1:def 6;
then A10:
f /. (i + 1) in rng f
by A9, FUNCT_1:3;
f /. (i + 1) in LSeg (f,i)
by A1, A6, TOPREAL1:21;
then
f /. (i + 1) in (LSeg (f,i)) /\ (rng f)
by A10, XBOOLE_0:def 4;
then
{(f /. i),(f /. (i + 1))} c= (LSeg (f,i)) /\ (rng f)
by A7, ZFMISC_1:32;
then
not (LSeg (f,i)) /\ (rng f) c= {(f /. i),(f /. (i + 1))}
by A5, XBOOLE_0:def 10;
then consider x being object such that
A11:
x in (LSeg (f,i)) /\ (rng f)
and
A12:
not x in {(f /. i),(f /. (i + 1))}
;
reconsider x = x as Point of (TOP-REAL 2) by A11;
A13:
x in LSeg (f,i)
by A11, XBOOLE_0:def 4;
x in rng f
by A11, XBOOLE_0:def 4;
then consider j being object such that
A14:
j in dom f
and
A15:
x = f . j
by FUNCT_1:def 3;
A16:
x = f /. j
by A14, A15, PARTFUN1:def 6;
reconsider j = j as Nat by A14;
A17:
1 <= j
by A14, FINSEQ_3:25;
reconsider j = j as Nat ;
A18:
x <> f /. i
by A12, TARSKI:def 2;
then A19:
j <> i
by A14, A15, PARTFUN1:def 6;
A20:
x <> f /. (i + 1)
by A12, TARSKI:def 2;
then A21:
j <> i + 1
by A14, A15, PARTFUN1:def 6;
now contradictionper cases
( j + 1 > len f or ( i < j & j + 1 <= len f ) or j < i )
by A19, XXREAL_0:1;
suppose A22:
j + 1
> len f
;
contradictionA23:
j <= len f
by A14, FINSEQ_3:25;
len f <= j
by A22, NAT_1:13;
then A24:
j = len f
by A23, XXREAL_0:1;
consider k being
Nat such that A25:
len f = 1
+ k
by A6, A8, NAT_1:10, XXREAL_0:2;
reconsider k =
k as
Nat ;
1
< len f
by A6, A8, XXREAL_0:2;
then
1
<= k
by A25, NAT_1:13;
then A26:
x in LSeg (
f,
k)
by A16, A24, A25, TOPREAL1:21;
i <= k
by A2, A25, NAT_1:13;
then
i < k
by A20, A16, A24, A25, XXREAL_0:1;
then A27:
i + 1
<= k
by NAT_1:13;
hence
contradiction
;
verum end; suppose that A29:
i < j
and A30:
j + 1
<= len f
;
contradiction
i + 1
<= j
by A29, NAT_1:13;
then
i + 1
< j
by A21, XXREAL_0:1;
then A31:
LSeg (
f,
i)
misses LSeg (
f,
j)
by TOPREAL1:def 7;
x in LSeg (
f,
j)
by A16, A17, A30, TOPREAL1:21;
hence
contradiction
by A13, A31, XBOOLE_0:3;
verum end; end; end;
hence
contradiction
; verum