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

( 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