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

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