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;
per cases ( q .. f < len f or q .. f = len f ) by A2, XXREAL_0:1;
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;
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;
end;