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

proof

let k be Element of NAT ; :: thesis: ( 1 <= k & k <= len q implies q . k in the carrier' of G )
assume ( 1 <= k & k <= len q ) ; :: thesis: q . k in the carrier' of G
then A2: k in dom q by FINSEQ_3:27;
dom q c= dom p by RELAT_1:89;
then ( 1 <= k & k <= len p ) by A2, FINSEQ_3:27;
then p . k in the carrier' of G by Def11;
hence q . k in the carrier' of G by A2, FUNCT_1:70; :: thesis: verum

end;

ex q1 being FinSequence st
( len q1 = (len q) + 1 & ( for n being Element of NAT st 1 <= n & n <= len q1 holds
q1 . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len q holds
ex x', y' being Vertex of G st
( x' = q1 . n & y' = q1 . (n + 1) & q . n joins x',y' ) ) )

proof

consider q1 being FinSequence such that
A3: ( len q1 = (len p) + 1 & ( for n being Element of NAT st 1 <= n & n <= len q1 holds
q1 . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len p holds
ex x', y' being Vertex of G st
( x' = q1 . n & y' = q1 . (n + 1) & p . n joins x',y' ) ) ) by Def11;
reconsider q2 = q1 | (Seg (n + 1)) as FinSequence by FINSEQ_1:19;
take q2 ; :: thesis: ( len q2 = (len q) + 1 & ( for n being Element of NAT st 1 <= n & n <= len q2 holds
q2 . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len q holds
ex x', y' being Vertex of G st
( x' = q2 . n & y' = q2 . (n + 1) & q . n joins x',y' ) ) )
thus A4: len q2 = (len q) + 1 :: thesis: ( ( for n being Element of NAT st 1 <= n & n <= len q2 holds
q2 . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len q holds
ex x', y' being Vertex of G st
( x' = q2 . n & y' = q2 . (n + 1) & q . n joins x',y' ) ) )

proof

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

A7: now

assume A8: (len p) + 1 <= n + 1 ; :: thesis: len q2 = (len q) + 1
then Seg ((len p) + 1) c= Seg (n + 1) by FINSEQ_1:7;
then dom q2 = Seg ((len p) + 1) by A5, XBOOLE_1:28;
then A9: len q2 = (len p) + 1 by FINSEQ_1:def 3;
len p <= n by A8, XREAL_1:8;
then Seg (len p) c= Seg n by FINSEQ_1:7;
then dom q = Seg (len p) by A6, XBOOLE_1:28;
hence len q2 = (len q) + 1 by A9, FINSEQ_1:def 3; :: thesis: verum

end;

now

assume A10: n + 1 <= (len p) + 1 ; :: thesis: len q2 = (len q) + 1
then Seg (n + 1) c= Seg ((len p) + 1) by FINSEQ_1:7;
then dom q2 = Seg (n + 1) by A5, XBOOLE_1:28;
then A11: len q2 = n + 1 by FINSEQ_1:def 3;
n <= len p by A10, XREAL_1:8;
then Seg n c= Seg (len p) by FINSEQ_1:7;
then dom q = Seg n by A6, XBOOLE_1:28;
hence len q2 = (len q) + 1 by A11, FINSEQ_1:def 3; :: thesis: verum

end;

hence len q2 = (len q) + 1 by A7; :: thesis: verum

end;

thus for n being Element of NAT st 1 <= n & n <= len q2 holds
q2 . n in the carrier of G :: thesis: for n being Element of NAT st 1 <= n & n <= len q holds
ex x', y' being Vertex of G st
( x' = q2 . n & y' = q2 . (n + 1) & q . n joins x',y' )

proof

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len q2 implies q2 . n in the carrier of G )
assume ( 1 <= n & n <= len q2 ) ; :: thesis: q2 . n in the carrier of G
then A12: n in dom q2 by FINSEQ_3:27;
dom q2 c= dom q1 by RELAT_1:89;
then ( 1 <= n & n <= len q1 ) by A12, FINSEQ_3:27;
then q1 . n in the carrier of G by A3;
hence q2 . n in the carrier of G by A12, FUNCT_1:70; :: thesis: verum

end;

let k be Element of NAT ; :: thesis: ( 1 <= k & k <= len q implies ex x', y' being Vertex of G st
( x' = q2 . k & y' = q2 . (k + 1) & q . k joins x',y' ) )
assume A13: ( 1 <= k & k <= len q ) ; :: thesis: ex x', y' being Vertex of G st
( x' = q2 . k & y' = q2 . (k + 1) & q . k joins x',y' )
then A14: k in dom q by FINSEQ_3:27;
dom q c= dom p by RELAT_1:89;
then ( 1 <= k & k <= len p ) by A14, FINSEQ_3:27;
then consider x', y' being Vertex of G such that
A15: ( x' = q1 . k & y' = q1 . (k + 1) & p . k joins x',y' ) by A3;
take x' ; :: thesis: ex y' being Vertex of G st
( x' = q2 . k & y' = q2 . (k + 1) & q . k joins x',y' )
take y' ; :: thesis: ( x' = q2 . k & y' = q2 . (k + 1) & q . k joins x',y' )
len q <= (len q) + 1 by NAT_1:11;
then ( 1 <= k & k <= len q2 ) by A4, A13, XXREAL_0:2;
then k in dom q2 by FINSEQ_3:27;
hence x' = q2 . k by A15, FUNCT_1:70; :: thesis: ( y' = q2 . (k + 1) & q . k joins x',y' )
A16: k + 1 <= len q2 by A4, A13, XREAL_1:9;
1 + 1 <= k + 1 by A13, XREAL_1:9;
then 1 <= k + 1 by XXREAL_0:2;
then k + 1 in dom q2 by A16, FINSEQ_3:27;
hence y' = q2 . (k + 1) by A15, FUNCT_1:70; :: thesis: q . k joins x',y'
thus q . k joins x',y' by A14, A15, FUNCT_1:70; :: thesis: verum

end;

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