let n be Nat; :: thesis:
let G be Graph; :: thesis:
let p be Chain of G; :: thesis:
reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:15;
A1: for n being Nat st 1 <= n & n <= len q holds
q . n in the carrier' of G

let k be Nat; :: thesis:
assume that
A2: 1 <= k and
A3: k <= len q ; :: thesis:
A4: k in dom q by A2, A3, FINSEQ_3:25;
dom q c= dom p by RELAT_1:60;
then k <= len p by A4, FINSEQ_3:25;
then p . k in the carrier' of G by A2, Def14;
hence q . k in the carrier' of G by A4, FUNCT_1:47; :: thesis:

end;

ex q1 being FinSequence st
( len q1 = (len q) + 1 & ( for n being Nat st 1 <= n & n <= len q1 holds
q1 . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len q holds
ex x9, y9 being Vertex of G st
( x9 = q1 . n & y9 = q1 . (n + 1) & q . n joins x9,y9 ) ) )

consider q1 being FinSequence such that
A5: len q1 = (len p) + 1 and
A6: for n being Nat st 1 <= n & n <= len q1 holds
q1 . n in the carrier of G and
A7: for n being Nat st 1 <= n & n <= len p holds
ex x9, y9 being Vertex of G st
( x9 = q1 . n & y9 = q1 . (n + 1) & p . n joins x9,y9 ) by Def14;
reconsider q2 = q1 | (Seg (n + 1)) as FinSequence by FINSEQ_1:15;
take q2 ; :: thesis:
thus A8: len q2 = (len q) + 1 :: thesis:

A9: dom q2 = (dom q1) /\ (Seg (n + 1)) by RELAT_1:61
.= (Seg ((len p) + 1)) /\ (Seg (n + 1)) by A5, FINSEQ_1:def 3 ;
A10: dom q = (dom p) /\ (Seg n) by RELAT_1:61
.= (Seg (len p)) /\ (Seg n) by FINSEQ_1:def 3 ;

per cases ) + 1 <= n + 1 or n + 1 <= (len p) + 1 ) ;

suppose A11: (len p) + 1 <= n + 1 ; :: thesis:

then Seg ((len p) + 1) c= Seg (n + 1) by FINSEQ_1:5;
then dom q2 = Seg ((len p) + 1) by A9, XBOOLE_1:28;
then A12: len q2 = (len p) + 1 by FINSEQ_1:def 3;
len p <= n by A11, XREAL_1:6;
then Seg (len p) c= Seg n by FINSEQ_1:5;
then dom q = Seg (len p) by A10, XBOOLE_1:28;
hence len q2 = (len q) + 1 by A12, FINSEQ_1:def 3; :: thesis:

end;

suppose A13: n + 1 <= (len p) + 1 ; :: thesis:

then Seg (n + 1) c= Seg ((len p) + 1) by FINSEQ_1:5;
then dom q2 = Seg (n + 1) by A9, XBOOLE_1:28;
then A14: len q2 = n + 1 by FINSEQ_1:def 3;
A15: n in NAT by ORDINAL1:def 12;
n <= len p by A13, XREAL_1:6;
then Seg n c= Seg (len p) by FINSEQ_1:5;
then dom q = Seg n by A10, XBOOLE_1:28;
hence len q2 = (len q) + 1 by A14, FINSEQ_1:def 3, A15; :: thesis:

end;

end;

end;

thus for n being Nat st 1 <= n & n <= len q2 holds
q2 . n in the carrier of G :: thesis:

let n be Nat; :: thesis:
assume that
A16: 1 <= n and
A17: n <= len q2 ; :: thesis:
A18: n in dom q2 by A16, A17, FINSEQ_3:25;
dom q2 c= dom q1 by RELAT_1:60;
then n <= len q1 by A18, FINSEQ_3:25;
then q1 . n in the carrier of G by A6, A16;
hence q2 . n in the carrier of G by A18, FUNCT_1:47; :: thesis:

end;

let k be Nat; :: thesis:
assume that
A19: 1 <= k and
A20: k <= len q ; :: thesis:
A21: k in dom q by A19, A20, FINSEQ_3:25;
dom q c= dom p by RELAT_1:60;
then k <= len p by A21, FINSEQ_3:25;
then consider x9, y9 being Vertex of G such that
A22: x9 = q1 . k and
A23: y9 = q1 . (k + 1) and
A24: p . k joins x9,y9 by A7, A19;
take x9 ; :: thesis:
take y9 ; :: thesis:
len q <= (len q) + 1 by NAT_1:11;
then k <= len q2 by A8, A20, XXREAL_0:2;
then k in dom q2 by A19, FINSEQ_3:25;
hence x9 = q2 . k by A22, FUNCT_1:47; :: thesis:
A25: k + 1 <= len q2 by A8, A20, XREAL_1:7;
1 + 1 <= k + 1 by A19, XREAL_1:7;
then 1 <= k + 1 by XXREAL_0:2;
then k + 1 in dom q2 by A25, FINSEQ_3:25;
hence y9 = q2 . (k + 1) by A23, FUNCT_1:47; :: thesis:
thus q . k joins x9,y9 by A21, A24, FUNCT_1:47; :: thesis:

end;

hence p | (Seg n) is Chain of G by A1, Def14; :: thesis: