let f be FinSequence of (TOP-REAL 2); :: thesis: 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); :: thesis: for i being Nat st p in rng f holds
LSeg (f :- p),(i + 1) = LSeg f,(i + (p .. f))
let i be Nat; :: thesis: ( 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 ; :: thesis: LSeg (f :- p),(i + 1) = LSeg f,(i + (p .. f))
then A3: len (f :- p) = ((len f) - (p .. f)) + 1 by FINSEQ_5:53;
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) ; :: thesis: LSeg (f :- p),(i + 1) = LSeg f,(i + (p .. f))

then i + 1 <= (len f) - (p .. f) by A4, A3, XREAL_1:8;
then A6: (i + 1) + (p .. f) <= len f by XREAL_1:21;
1 <= p .. f by A2, FINSEQ_4:31;
then i + 1 <= i + (p .. f) by XREAL_1:8;
then A7: 1 <= i + (p .. f) by A1, XXREAL_0:2;
A8: i + 1 in dom (f :- p) by A1, A4, A5, SEQ_4:151;
A9: (i + 1) + 1 in dom (f :- p) by A1, A5, SEQ_4:151;
thus LSeg (f :- p),(i + 1) = LSeg ((f :- p) /. (i + 1)),((f :- p) /. ((i + 1) + 1)) by A1, A5, TOPREAL1:def 5
.= LSeg (f /. (i + (p .. f))),((f :- p) /. ((i + 1) + 1)) by A2, A8, FINSEQ_5:55
.= LSeg (f /. (i + (p .. f))),(f /. ((i + 1) + (p .. f))) by A2, A9, FINSEQ_5:55
.= LSeg (f /. (i + (p .. f))),(f /. ((i + (p .. f)) + 1))
.= LSeg f,(i + (p .. f)) by A7, A6, TOPREAL1:def 5 ; :: thesis: verum

end;

suppose A10: i + 2 > len (f :- p) ; :: thesis: LSeg (f :- p),(i + 1) = LSeg f,(i + (p .. f))

then i + 1 > (len f) - (p .. f) by A4, A3, XREAL_1:8;
then (p .. f) + (i + 1) > len f by XREAL_1:21;
then (i + (p .. f)) + 1 > len f ;
hence LSeg f,(i + (p .. f)) = {} by TOPREAL1:def 5
.= LSeg (f :- p),(i + 1) by A4, A10, TOPREAL1:def 5 ;
:: thesis: verum

end;

end;