let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st not f is empty holds
L~ (f ^ <*p*>) = (L~ f) \/ (LSeg (f /. (len f)),p)
let p be Point of (TOP-REAL 2); :: thesis: ( not f is empty implies L~ (f ^ <*p*>) = (L~ f) \/ (LSeg (f /. (len f)),p) )
set fp = f ^ <*p*>;
A1: (len f) + 1 <= len (f ^ <*p*>) by FINSEQ_2:19;
1 <= (len f) + 1 by NAT_1:11;
then A2: (len f) + 1 in dom (f ^ <*p*>) by A1, FINSEQ_3:27;
A3: (f ^ <*p*>) /. ((len f) + 1) = p by FINSEQ_4:82;
len (f ^ <*p*>) = (len f) + 1 by FINSEQ_2:19;
then A4: (f ^ <*p*>) | ((len f) + 1) = f ^ <*p*> by FINSEQ_1:79;
A5: dom f c= dom (f ^ <*p*>) by FINSEQ_1:39;
A6: (f ^ <*p*>) | (len f) = f by FINSEQ_5:26;
assume not f is empty ; :: thesis: L~ (f ^ <*p*>) = (L~ f) \/ (LSeg (f /. (len f)),p)
then A7: len f in dom f by FINSEQ_5:6;
then (f ^ <*p*>) /. (len f) = f /. (len f) by FINSEQ_4:83;
hence L~ (f ^ <*p*>) = (L~ f) \/ (LSeg (f /. (len f)),p) by A2, A7, A3, A4, A5, A6, TOPREAL3:45; :: thesis: verum