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: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) ; :: thesis: 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 ; :: 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:6;
then (p .. f) + (i + 1) > len f by XREAL_1:19;
then (i + (p .. f)) + 1 > len f ;
hence LSeg (f,(i + (p .. f))) = {} by TOPREAL1:def 3
.= LSeg ((f :- p),(i + 1)) by A4, A10, TOPREAL1:def 3 ;
:: thesis: verum

end;

end;