let f, h be FinSequence of (TOP-REAL 2); :: thesis: for i being Element of NAT st f /. i <> f /. 1 & 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 Element of NAT ; :: thesis: ( f /. i <> f /. 1 & 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 A1: ( f /. i <> f /. 1 & f is being_S-Seq & i > 2 & i in dom f & 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)) )
then A2: ( h is being_S-Seq & h = f | (Seg i) & Seg (len f) = dom f & Seg (len h) = dom h ) by FINSEQ_1:def 3, FINSEQ_1:def 15, TOPREAL3:40;
then i <= len f by A1, FINSEQ_1:3;
then ( Seg i c= Seg (len f) & dom h = (Seg (len f)) /\ (Seg i) ) by A2, FINSEQ_1:7, RELAT_1:90;
then ( dom h = Seg i & 1 <= i ) by A1, A2, FINSEQ_1:3, XBOOLE_1:28;
then ( 1 in dom h & i in dom h & len h = i ) by FINSEQ_1:3, FINSEQ_1:def 3;
hence ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. i ) by A1, FINSEQ_4:85, TOPREAL3:40; :: 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 A3: ( L~ h is_S-P_arc_joining f /. 1,f /. i & L~ h c= L~ f ) by A1, Def1, TOPREAL3:27; :: thesis: L~ h = (L~ (f | i)) \/ (LSeg (f /. i),(f /. i))
A4: LSeg (f /. i),(f /. i) = {(f /. i)} by RLTOPSP1:71;
f /. i in L~ (f | i) by A1, A3, Th4;
then {(f /. i)} c= L~ (f | i) by ZFMISC_1:37;
hence L~ h = (L~ (f | i)) \/ (LSeg (f /. i),(f /. i)) by A1, A4, XBOOLE_1:12; :: thesis: verum