let f, h be FinSequence of (); :: 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 ;
then A5: Seg i c= Seg (len f) by FINSEQ_1:5;
h = f | (Seg i) by ;
then dom h = (Seg (len f)) /\ (Seg i) by ;
then A6: dom h = Seg i by ;
1 <= i by ;
then A7: ( 1 in dom h & i in dom h ) by ;
i in NAT by ORDINAL1:def 12;
then len h = i by ;
hence ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. i ) by ; :: 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 ; :: thesis: L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. i)))
then f /. i in L~ (f | i) by ;
then ( LSeg ((f /. i),(f /. i)) = {(f /. i)} & {(f /. i)} c= L~ (f | i) ) by ;
hence L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. i))) by ; :: thesis: verum