let p be Point of (); :: thesis: for f being FinSequence of ()
for n being Nat st p <> f /. 1 & f is being_S-Seq & p in LSeg (f,n) holds
ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

let f be FinSequence of (); :: thesis: for n being Nat st p <> f /. 1 & f is being_S-Seq & p in LSeg (f,n) holds
ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

let n be Nat; :: thesis: ( p <> f /. 1 & f is being_S-Seq & p in LSeg (f,n) implies ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) )

set p1 = f /. 1;
set q = f /. n;
assume that
A1: p <> f /. 1 and
A2: f is being_S-Seq and
A3: p in LSeg (f,n) ; :: thesis: ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

A4: f is special by A2;
A5: n <= n + 1 by NAT_1:11;
A6: now :: thesis: ( n in dom f & n + 1 in dom f )
assume A7: ( not n in dom f or not n + 1 in dom f ) ; :: thesis: contradiction
now :: thesis: contradictionend;
hence contradiction ; :: thesis: verum
end;
A8: f is one-to-one by A2;
A9: Seg (len f) = dom f by FINSEQ_1:def 3;
then A10: 1 <= n by ;
A11: n + 1 <= len f by ;
A12: n <= len f by ;
now :: thesis: ( ( f /. n = p & f /. (n + 1) = p & contradiction ) or ( f /. n = p & f /. (n + 1) <> p & ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) ) or ( f /. n <> p & f /. (n + 1) = p & ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) ) or ( f /. n <> p & f /. (n + 1) <> p & ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) ) )
per cases ( ( f /. n = p & f /. (n + 1) = p ) or ( f /. n = p & f /. (n + 1) <> p ) or ( f /. n <> p & f /. (n + 1) = p ) or ( f /. n <> p & f /. (n + 1) <> p ) ) ;
case ( f /. n = p & f /. (n + 1) = p ) ; :: thesis: contradiction
end;
case A13: ( f /. n = p & f /. (n + 1) <> p ) ; :: thesis: ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

then 1 < n by ;
then A14: 1 + 1 <= n by NAT_1:13;
now :: thesis: ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )
per cases ( n = 1 + 1 or n > 2 ) by ;
suppose A15: n = 1 + 1 ; :: thesis: ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

now :: thesis: ex h being FinSequence of the carrier of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )
per cases ) `1 = p `1 or (f /. 1) `2 = p `2 ) by A4, A12, A13, A15;
suppose A16: (f /. 1) `1 = p `1 ; :: thesis: ex h being FinSequence of the carrier of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

take h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p*>; :: thesis: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )
thus ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by A1, A2, A13, A15, A16, Th15; :: thesis: verum
end;
suppose A17: (f /. 1) `2 = p `2 ; :: thesis: ex h being FinSequence of the carrier of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

take h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*>; :: thesis: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )
thus ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by A1, A2, A13, A15, A17, Th14; :: thesis: verum
end;
end;
end;
hence ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) ; :: thesis: verum
end;
suppose A18: n > 2 ; :: thesis: ex h being FinSequence of the carrier of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

take h = f | n; :: thesis: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )
thus ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by A2, A6, A13, A18, Th16; :: thesis: verum
end;
end;
end;
hence ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) ; :: thesis: verum
end;
case A19: ( f /. n <> p & f /. (n + 1) = p ) ; :: thesis: ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

now :: thesis: ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )
per cases ( n = 1 or 1 < n ) by ;
suppose A20: n = 1 ; :: thesis: ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

now :: thesis: ex h being FinSequence of the carrier of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )
per cases ) `1 = p `1 or (f /. 1) `2 = p `2 ) by A4, A11, A19, A20;
suppose A21: (f /. 1) `1 = p `1 ; :: thesis: ex h being FinSequence of the carrier of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

take h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p*>; :: thesis: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )
thus ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by A2, A19, A20, A21, Th15; :: thesis: verum
end;
suppose A22: (f /. 1) `2 = p `2 ; :: thesis: ex h being FinSequence of the carrier of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

take h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*>; :: thesis: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )
thus ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by A2, A19, A20, A22, Th14; :: thesis: verum
end;
end;
end;
hence ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) ; :: thesis: verum
end;
suppose A23: 1 < n ; :: thesis: ex h being FinSequence of the carrier of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

take h = f | (n + 1); :: thesis: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )
1 + 1 < n + 1 by ;
hence ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by ; :: thesis: verum
end;
end;
end;
hence ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) ; :: thesis: verum
end;
case A24: ( f /. n <> p & f /. (n + 1) <> p ) ; :: thesis: ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

now :: thesis: ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )
per cases ( n = 1 or 1 < n ) by ;
suppose A25: n = 1 ; :: thesis: ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

set q1 = f /. (1 + 1);
A26: len f >= 1 + 1 by A2;
then A27: LSeg (f,n) = LSeg ((f /. 1),(f /. (1 + 1))) by ;
now :: thesis: ex h being FinSequence of the carrier of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )
per cases ) `1 = (f /. (1 + 1)) `1 or (f /. 1) `2 = (f /. (1 + 1)) `2 ) by ;
suppose A28: (f /. 1) `1 = (f /. (1 + 1)) `1 ; :: thesis: ex h being FinSequence of the carrier of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

take h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p*>; :: thesis: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )
( (f /. 1) `1 <= p `1 & p `1 <= (f /. (1 + 1)) `1 ) by ;
then (f /. 1) `1 = p `1 by ;
hence ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by A1, A2, A3, A25, Th12; :: thesis: verum
end;
suppose A29: (f /. 1) `2 = (f /. (1 + 1)) `2 ; :: thesis: ex h being FinSequence of the carrier of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

take h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*>; :: thesis: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )
( (f /. 1) `2 <= p `2 & p `2 <= (f /. (1 + 1)) `2 ) by ;
then (f /. 1) `2 = p `2 by ;
hence ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by A1, A2, A3, A25, Th11; :: thesis: verum
end;
end;
end;
hence ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) ; :: thesis: verum
end;
suppose A30: 1 < n ; :: thesis: ex h being FinSequence of the carrier of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

take h = (f | n) ^ <*p*>; :: thesis: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )
thus ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by A2, A3, A6, A24, A30, Th13; :: thesis: verum
end;
end;
end;
hence ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) ; :: thesis: verum
end;
end;
end;
hence ex h being FinSequence of () st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) ; :: thesis: verum