let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Nat st f is unfolded & f is s.n.c. & f is one-to-one & f /. (len f) in LSeg (f,i) & i in dom f & i + 1 in dom f holds

i + 1 = len f

let i be Nat; :: thesis: ( f is unfolded & f is s.n.c. & f is one-to-one & f /. (len f) in LSeg (f,i) & i in dom f & i + 1 in dom f implies i + 1 = len f )

assume that

A1: f is unfolded and

A2: f is s.n.c. and

A3: f is one-to-one and

A4: f /. (len f) in LSeg (f,i) and

A5: i in dom f and

A6: i + 1 in dom f and

A7: i + 1 <> len f ; :: thesis: contradiction

A8: 1 <= i by A5, FINSEQ_3:25;

A9: i <= len f by A5, FINSEQ_3:25;

then reconsider l = (len f) - 1 as Element of NAT by A8, INT_1:5, XXREAL_0:2;

1 <= len f by A8, A9, XXREAL_0:2;

then A10: l + 1 in dom f by FINSEQ_3:25;

A11: i + 1 <= len f by A6, FINSEQ_3:25;

then i + 1 < len f by A7, XXREAL_0:1;

then A12: (i + 1) + 1 <= len f by NAT_1:13;

then A13: i + 1 <= (len f) - 1 by XREAL_1:19;

i <= l by A11, XREAL_1:19;

then A14: 1 <= l by A8, XXREAL_0:2;

then A15: f /. (l + 1) in LSeg (f,l) by TOPREAL1:21;

1 <= i + 1 by A6, FINSEQ_3:25;

then A16: f /. (i + 2) in LSeg (f,(i + 1)) by A12, TOPREAL1:21;

l <= len f by XREAL_1:43;

then A17: l in dom f by A14, FINSEQ_3:25;

l <> l + 1 ;

then A18: f /. l <> f /. (l + 1) by A3, A17, A10, PARTFUN2:10;

(i + 1) + 1 = i + (1 + 1) ;

then A19: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A1, A8, A12;

i + 1 = len f

let i be Nat; :: thesis: ( f is unfolded & f is s.n.c. & f is one-to-one & f /. (len f) in LSeg (f,i) & i in dom f & i + 1 in dom f implies i + 1 = len f )

assume that

A1: f is unfolded and

A2: f is s.n.c. and

A3: f is one-to-one and

A4: f /. (len f) in LSeg (f,i) and

A5: i in dom f and

A6: i + 1 in dom f and

A7: i + 1 <> len f ; :: thesis: contradiction

A8: 1 <= i by A5, FINSEQ_3:25;

A9: i <= len f by A5, FINSEQ_3:25;

then reconsider l = (len f) - 1 as Element of NAT by A8, INT_1:5, XXREAL_0:2;

1 <= len f by A8, A9, XXREAL_0:2;

then A10: l + 1 in dom f by FINSEQ_3:25;

A11: i + 1 <= len f by A6, FINSEQ_3:25;

then i + 1 < len f by A7, XXREAL_0:1;

then A12: (i + 1) + 1 <= len f by NAT_1:13;

then A13: i + 1 <= (len f) - 1 by XREAL_1:19;

i <= l by A11, XREAL_1:19;

then A14: 1 <= l by A8, XXREAL_0:2;

then A15: f /. (l + 1) in LSeg (f,l) by TOPREAL1:21;

1 <= i + 1 by A6, FINSEQ_3:25;

then A16: f /. (i + 2) in LSeg (f,(i + 1)) by A12, TOPREAL1:21;

l <= len f by XREAL_1:43;

then A17: l in dom f by A14, FINSEQ_3:25;

l <> l + 1 ;

then A18: f /. l <> f /. (l + 1) by A3, A17, A10, PARTFUN2:10;

(i + 1) + 1 = i + (1 + 1) ;

then A19: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A1, A8, A12;

now :: thesis: contradiction

hence
contradiction
; :: thesis: verumend;