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 that
A2: 1 <= k and
A3: k <= len q ; :: thesis: q . k in the carrier' of G
A4: k in dom q by A2, A3, FINSEQ_3:27;
dom q c= dom p by RELAT_1:89;
then k <= len p by A4, FINSEQ_3:27;
then p . k in the carrier' of G by A2, Def12;
hence q . k in the carrier' of G by A4, 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 x9, y9 being Vertex of G st
( x9 = q1 . n & y9 = q1 . (n + 1) & q . n joins x9,y9 ) ) )

proof

consider q1 being FinSequence such that
A9: len q1 = (len p) + 1 and
A10: for n being Element of NAT st 1 <= n & n <= len q1 holds
q1 . n in the carrier of G and
A11: for n being Element of 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 Def12;
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 x9, y9 being Vertex of G st
( x9 = q2 . n & y9 = q2 . (n + 1) & q . n joins x9,y9 ) ) )
thus A12: 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 x9, y9 being Vertex of G st
( x9 = q2 . n & y9 = q2 . (n + 1) & q . n joins x9,y9 ) ) )

proof

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

A15: now

assume A16: (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 A13, XBOOLE_1:28;
then A19: len q2 = (len p) + 1 by FINSEQ_1:def 3;
len p <= n by A16, XREAL_1:8;
then Seg (len p) c= Seg n by FINSEQ_1:7;
then dom q = Seg (len p) by A14, XBOOLE_1:28;
hence len q2 = (len q) + 1 by A19, FINSEQ_1:def 3; :: thesis: verum

end;

now

assume A24: 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 A13, XBOOLE_1:28;
then A27: len q2 = n + 1 by FINSEQ_1:def 3;
n <= len p by A24, XREAL_1:8;
then Seg n c= Seg (len p) by FINSEQ_1:7;
then dom q = Seg n by A14, XBOOLE_1:28;
hence len q2 = (len q) + 1 by A27, FINSEQ_1:def 3; :: thesis: verum

end;

hence len q2 = (len q) + 1 by A15; :: 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 x9, y9 being Vertex of G st
( x9 = q2 . n & y9 = q2 . (n + 1) & q . n joins x9,y9 )

proof

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

end;

let k be Element of NAT ; :: thesis: ( 1 <= k & k <= len q implies ex x9, y9 being Vertex of G st
( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 ) )
assume that
A37: 1 <= k and
A38: k <= len q ; :: thesis: ex x9, y9 being Vertex of G st
( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 )
A39: k in dom q by A37, A38, FINSEQ_3:27;
dom q c= dom p by RELAT_1:89;
then k <= len p by A39, FINSEQ_3:27;
then consider x9, y9 being Vertex of G such that
A42: x9 = q1 . k and
A43: y9 = q1 . (k + 1) and
A44: p . k joins x9,y9 by A11, A37;
take x9 ; :: thesis: ex y9 being Vertex of G st
( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 )
take y9 ; :: thesis: ( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 )
len q <= (len q) + 1 by NAT_1:11;
then k <= len q2 by A12, A38, XXREAL_0:2;
then k in dom q2 by A37, FINSEQ_3:27;
hence x9 = q2 . k by A42, FUNCT_1:70; :: thesis: ( y9 = q2 . (k + 1) & q . k joins x9,y9 )
A48: k + 1 <= len q2 by A12, A38, XREAL_1:9;
1 + 1 <= k + 1 by A37, XREAL_1:9;
then 1 <= k + 1 by XXREAL_0:2;
then k + 1 in dom q2 by A48, FINSEQ_3:27;
hence y9 = q2 . (k + 1) by A43, FUNCT_1:70; :: thesis: q . k joins x9,y9
thus q . k joins x9,y9 by A39, A44, FUNCT_1:70; :: thesis: verum

end;

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