let f be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2)
for i being Nat st p in rng f holds
LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f)))
let p be Point of (TOP-REAL 2); for i being Nat st p in rng f holds
LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f)))
let i be Nat; ( p in rng f implies LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f))) )
A1:
1 <= i + 1
by NAT_1:11;
assume A2:
p in rng f
; LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f)))
then A3:
len (f :- p) = ((len f) - (p .. f)) + 1
by FINSEQ_5:50;
A4:
i + (1 + 1) = (i + 1) + 1
;
per cases
( i + 2 <= len (f :- p) or i + 2 > len (f :- p) )
;
suppose A5:
i + 2
<= len (f :- p)
;
LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f)))then
i + 1
<= (len f) - (p .. f)
by A4, A3, XREAL_1:6;
then A6:
(i + 1) + (p .. f) <= len f
by XREAL_1:19;
1
<= p .. f
by A2, FINSEQ_4:21;
then
i + 1
<= i + (p .. f)
by XREAL_1:6;
then A7:
1
<= i + (p .. f)
by A1, XXREAL_0:2;
A8:
i + 1
in dom (f :- p)
by A1, A4, A5, SEQ_4:134;
A9:
(i + 1) + 1
in dom (f :- p)
by A1, A5, SEQ_4:134;
thus LSeg (
(f :- p),
(i + 1)) =
LSeg (
((f :- p) /. (i + 1)),
((f :- p) /. ((i + 1) + 1)))
by A1, A5, TOPREAL1:def 3
.=
LSeg (
(f /. (i + (p .. f))),
((f :- p) /. ((i + 1) + 1)))
by A2, A8, FINSEQ_5:52
.=
LSeg (
(f /. (i + (p .. f))),
(f /. ((i + 1) + (p .. f))))
by A2, A9, FINSEQ_5:52
.=
LSeg (
(f /. (i + (p .. f))),
(f /. ((i + (p .. f)) + 1)))
.=
LSeg (
f,
(i + (p .. f)))
by A7, A6, TOPREAL1:def 3
;
verum end; end;