let f be FinSequence of (TOP-REAL 2); :: thesis: for q being Point of (TOP-REAL 2) st q in rng f holds

L~ f = (L~ (f -: q)) \/ (L~ (f :- q))

let q be Point of (TOP-REAL 2); :: thesis: ( q in rng f implies L~ f = (L~ (f -: q)) \/ (L~ (f :- q)) )

set n = q .. f;

assume A1: q in rng f ; :: thesis: L~ f = (L~ (f -: q)) \/ (L~ (f :- q))

then A2: q .. f <= len f by FINSEQ_4:21;

L~ f = (L~ (f -: q)) \/ (L~ (f :- q))

let q be Point of (TOP-REAL 2); :: thesis: ( q in rng f implies L~ f = (L~ (f -: q)) \/ (L~ (f :- q)) )

set n = q .. f;

assume A1: q in rng f ; :: thesis: L~ f = (L~ (f -: q)) \/ (L~ (f :- q))

then A2: q .. f <= len f by FINSEQ_4:21;

per cases
( q .. f < len f or q .. f = len f )
by A2, XXREAL_0:1;

end;

suppose A3:
q .. f < len f
; :: thesis: L~ f = (L~ (f -: q)) \/ (L~ (f :- q))

then
len (f /^ (q .. f)) = (len f) - (q .. f)
by RFINSEQ:def 1;

then len (f /^ (q .. f)) <> 0 by A3;

then A4: not f /^ (q .. f) is empty ;

A5: len (f | (q .. f)) = q .. f by A3, FINSEQ_1:59;

f | (q .. f) = f -: q by FINSEQ_5:def 1;

then A6: (f | (q .. f)) /. (len (f | (q .. f))) = q by A1, A5, FINSEQ_5:45;

A7: (f | (q .. f)) ^ (f /^ (q .. f)) = f by RFINSEQ:8;

not f | (q .. f) is empty by A1, A5, FINSEQ_4:21;

hence L~ f = ((L~ (f | (q .. f))) \/ (LSeg (((f | (q .. f)) /. (len (f | (q .. f)))),((f /^ (q .. f)) /. 1)))) \/ (L~ (f /^ (q .. f))) by A4, A7, Th23

.= (L~ (f | (q .. f))) \/ ((LSeg (((f | (q .. f)) /. (len (f | (q .. f)))),((f /^ (q .. f)) /. 1))) \/ (L~ (f /^ (q .. f)))) by XBOOLE_1:4

.= (L~ (f | (q .. f))) \/ (L~ (<*((f | (q .. f)) /. (len (f | (q .. f))))*> ^ (f /^ (q .. f)))) by A4, Th20

.= (L~ (f | (q .. f))) \/ (L~ (f :- q)) by A6, FINSEQ_5:def 2

.= (L~ (f -: q)) \/ (L~ (f :- q)) by FINSEQ_5:def 1 ;

:: thesis: verum

end;then len (f /^ (q .. f)) <> 0 by A3;

then A4: not f /^ (q .. f) is empty ;

A5: len (f | (q .. f)) = q .. f by A3, FINSEQ_1:59;

f | (q .. f) = f -: q by FINSEQ_5:def 1;

then A6: (f | (q .. f)) /. (len (f | (q .. f))) = q by A1, A5, FINSEQ_5:45;

A7: (f | (q .. f)) ^ (f /^ (q .. f)) = f by RFINSEQ:8;

not f | (q .. f) is empty by A1, A5, FINSEQ_4:21;

hence L~ f = ((L~ (f | (q .. f))) \/ (LSeg (((f | (q .. f)) /. (len (f | (q .. f)))),((f /^ (q .. f)) /. 1)))) \/ (L~ (f /^ (q .. f))) by A4, A7, Th23

.= (L~ (f | (q .. f))) \/ ((LSeg (((f | (q .. f)) /. (len (f | (q .. f)))),((f /^ (q .. f)) /. 1))) \/ (L~ (f /^ (q .. f)))) by XBOOLE_1:4

.= (L~ (f | (q .. f))) \/ (L~ (<*((f | (q .. f)) /. (len (f | (q .. f))))*> ^ (f /^ (q .. f)))) by A4, Th20

.= (L~ (f | (q .. f))) \/ (L~ (f :- q)) by A6, FINSEQ_5:def 2

.= (L~ (f -: q)) \/ (L~ (f :- q)) by FINSEQ_5:def 1 ;

:: thesis: verum

suppose A8:
q .. f = len f
; :: thesis: L~ f = (L~ (f -: q)) \/ (L~ (f :- q))

then len (f /^ (q .. f)) =
(len f) - (q .. f)
by RFINSEQ:def 1

.= 0 by A8 ;

then A9: f /^ (q .. f) is empty ;

f :- q = <*q*> ^ (f /^ (q .. f)) by FINSEQ_5:def 2

.= <*q*> by A9, FINSEQ_1:34 ;

then A10: L~ (f :- q) is empty by Th12;

L~ f = L~ (f | (q .. f)) by A8, FINSEQ_1:58

.= L~ (f -: q) by FINSEQ_5:def 1 ;

hence L~ f = (L~ (f -: q)) \/ (L~ (f :- q)) by A10; :: thesis: verum

end;.= 0 by A8 ;

then A9: f /^ (q .. f) is empty ;

f :- q = <*q*> ^ (f /^ (q .. f)) by FINSEQ_5:def 2

.= <*q*> by A9, FINSEQ_1:34 ;

then A10: L~ (f :- q) is empty by Th12;

L~ f = L~ (f | (q .. f)) by A8, FINSEQ_1:58

.= L~ (f -: q) by FINSEQ_5:def 1 ;

hence L~ f = (L~ (f -: q)) \/ (L~ (f :- q)) by A10; :: thesis: verum