let f be FinSequence of (TOP-REAL 2); for k being Nat st 1 < k & len f = k + 1 & f is unfolded & f is s.n.c. holds
(L~ (f | k)) /\ (LSeg (f,k)) = {(f /. k)}
let k be Nat; ( 1 < k & len f = k + 1 & f is unfolded & f is s.n.c. implies (L~ (f | k)) /\ (LSeg (f,k)) = {(f /. k)} )
assume that
A1:
1 < k
and
A2:
len f = k + 1
and
A3:
f is unfolded
and
A4:
f is s.n.c.
; (L~ (f | k)) /\ (LSeg (f,k)) = {(f /. k)}
set f1 = f | k;
A5:
len (f | k) = k
by A2, FINSEQ_1:59, NAT_1:11;
reconsider k1 = k - 1 as Element of NAT by A1, INT_1:5;
set f2 = (f | k) | k1;
set l2 = { (LSeg (((f | k) | k1),m)) where m is Nat : ( 1 <= m & m + 1 <= len ((f | k) | k1) ) } ;
A6:
dom (f | k) = Seg (len (f | k))
by FINSEQ_1:def 3;
A7:
k in Seg k
by A1, FINSEQ_1:1;
A8:
dom ((f | k) | k1) = Seg (len ((f | k) | k1))
by FINSEQ_1:def 3;
A9:
k1 < k
by XREAL_1:44;
A10:
k1 <= k
by XREAL_1:44;
then A11:
len ((f | k) | k1) = k1
by A5, FINSEQ_1:59;
A12:
Seg k1 c= Seg k
by A10, FINSEQ_1:5;
L~ ((f | k) | k1) misses LSeg (f,k)
proof
assume
not
L~ ((f | k) | k1) misses LSeg (
f,
k)
;
contradiction
then consider x being
object such that A13:
x in L~ ((f | k) | k1)
and A14:
x in LSeg (
f,
k)
by XBOOLE_0:3;
consider X being
set such that A15:
x in X
and A16:
X in { (LSeg (((f | k) | k1),m)) where m is Nat : ( 1 <= m & m + 1 <= len ((f | k) | k1) ) }
by A13, TARSKI:def 4;
consider n being
Nat such that A17:
X = LSeg (
((f | k) | k1),
n)
and A18:
1
<= n
and A19:
n + 1
<= len ((f | k) | k1)
by A16;
A20:
(
n in dom ((f | k) | k1) &
n + 1
in dom ((f | k) | k1) )
by A18, A19, SEQ_4:134;
then
LSeg (
((f | k) | k1),
n)
= LSeg (
(f | k),
n)
by TOPREAL3:17;
then
LSeg (
((f | k) | k1),
n)
= LSeg (
f,
n)
by A6, A12, A8, A5, A11, A20, TOPREAL3:17;
then A21:
LSeg (
f,
n)
meets LSeg (
f,
k)
by A14, A15, A17, XBOOLE_0:3;
n + 1
< k
by A9, A11, A19, XXREAL_0:2;
hence
contradiction
by A4, A21;
verum
end;
then A22:
(L~ ((f | k) | k1)) /\ (LSeg (f,k)) = {}
;
A23:
k + 1 = k1 + (1 + 1)
;
1 + 1 <= k
by A1, NAT_1:13;
then A24:
1 <= k1
by XREAL_1:19;
then A25:
k1 in Seg k
by A10, FINSEQ_1:1;
k1 + 1 in Seg k
by A1, FINSEQ_1:1;
then
L~ (f | k) = (L~ ((f | k) | k1)) \/ (LSeg ((f | k),k1))
by A24, A5, Th3;
hence (L~ (f | k)) /\ (LSeg (f,k)) =
{} \/ ((LSeg ((f | k),k1)) /\ (LSeg (f,k)))
by A22, XBOOLE_1:23
.=
(LSeg (f,k1)) /\ (LSeg (f,(k1 + 1)))
by A6, A7, A25, A5, TOPREAL3:17
.=
{(f /. k)}
by A2, A3, A24, A23
;
verum