let f, h be FinSequence of (TOP-REAL 2); :: thesis: for i being Nat st f is being_S-Seq & i > 2 & i in dom f & h = f | i holds
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. i & L~ h is_S-P_arc_joining f /. 1,f /. i & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. i))) )
let i be Nat; :: thesis: ( f is being_S-Seq & i > 2 & i in dom f & h = f | i implies ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. i & L~ h is_S-P_arc_joining f /. 1,f /. i & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. i))) ) )
assume that
A1: ( f is being_S-Seq & i > 2 ) and
A2: i in dom f and
A3: h = f | i ; :: thesis: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. i & L~ h is_S-P_arc_joining f /. 1,f /. i & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. i))) )
A4: Seg (len f) = dom f by FINSEQ_1:def 3;
then i <= len f by A2, FINSEQ_1:1;
then A5: Seg i c= Seg (len f) by FINSEQ_1:5;
h = f | (Seg i) by A3, FINSEQ_1:def 15;
then dom h = (Seg (len f)) /\ (Seg i) by A4, RELAT_1:61;
then A6: dom h = Seg i by A5, XBOOLE_1:28;
1 <= i by A2, A4, FINSEQ_1:1;
then A7: ( 1 in dom h & i in dom h ) by A6, FINSEQ_1:1;
i in NAT by ORDINAL1:def 12;
then len h = i by A6, FINSEQ_1:def 3;
hence ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. i ) by A1, A2, A3, A7, FINSEQ_4:70, TOPREAL3:33; :: thesis: ( L~ h is_S-P_arc_joining f /. 1,f /. i & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. i))) )
hence ( L~ h is_S-P_arc_joining f /. 1,f /. i & L~ h c= L~ f ) by A3, TOPREAL3:20; :: thesis: L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. i)))
then f /. i in L~ (f | i) by A3, Th3;
then ( LSeg ((f /. i),(f /. i)) = {(f /. i)} & {(f /. i)} c= L~ (f | i) ) by RLTOPSP1:70, ZFMISC_1:31;
hence L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. i))) by A3, XBOOLE_1:12; :: thesis: verum