let f, h be FinSequence of (TOP-REAL 2); 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; ( 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
; ( 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; ( 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; 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; verum