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:16;
1 <= (len f) + 1 by NAT_1:11;
then A2: (len f) + 1 in dom (f ^ <*p*>) by A1, FINSEQ_3:25;
A3: (f ^ <*p*>) /. ((len f) + 1) = p by FINSEQ_4:67;
len (f ^ <*p*>) = (len f) + 1 by FINSEQ_2:16;
then A4: (f ^ <*p*>) | ((len f) + 1) = f ^ <*p*> by FINSEQ_1:58;
A5: dom f c= dom (f ^ <*p*>) by FINSEQ_1:26;
A6: (f ^ <*p*>) | (len f) = f by FINSEQ_5:23;
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:68;
hence L~ (f ^ <*p*>) = (L~ f) \/ (LSeg ((f /. (len f)),p)) by A2, A7, A3, A4, A5, A6, TOPREAL3:38; :: thesis: verum