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;
A5: dom q c= dom p by RELAT_1:89;
A6: k <= len p by A4, A5, FINSEQ_3:27;
A7: p . k in the carrier' of G by A2, A6, Def12;
thus q . k in the carrier' of G by A4, A7, FUNCT_1:70; :: thesis: verum

end;

A8: 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
A17: Seg ((len p) + 1) c= Seg (n + 1) by A16, FINSEQ_1:7;
A18: dom q2 = Seg ((len p) + 1) by A13, A17, XBOOLE_1:28;
A19: len q2 = (len p) + 1 by A18, FINSEQ_1:def 3;
A20: len p <= n by A16, XREAL_1:8;
A21: Seg (len p) c= Seg n by A20, FINSEQ_1:7;
A22: dom q = Seg (len p) by A14, A21, XBOOLE_1:28;
thus len q2 = (len q) + 1 by A19, A22, FINSEQ_1:def 3; :: thesis: verum

end;

A23: now

assume A24: n + 1 <= (len p) + 1 ; :: thesis: len q2 = (len q) + 1
A25: Seg (n + 1) c= Seg ((len p) + 1) by A24, FINSEQ_1:7;
A26: dom q2 = Seg (n + 1) by A13, A25, XBOOLE_1:28;
A27: len q2 = n + 1 by A26, FINSEQ_1:def 3;
A28: n <= len p by A24, XREAL_1:8;
A29: Seg n c= Seg (len p) by A28, FINSEQ_1:7;
A30: dom q = Seg n by A14, A29, XBOOLE_1:28;
thus len q2 = (len q) + 1 by A27, A30, FINSEQ_1:def 3; :: thesis: verum

end;

thus len q2 = (len q) + 1 by A15, A23; :: 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;
A34: dom q2 c= dom q1 by RELAT_1:89;
A35: n <= len q1 by A33, A34, FINSEQ_3:27;
A36: q1 . n in the carrier of G by A10, A31, A35;
thus q2 . n in the carrier of G by A33, A36, 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;
A40: dom q c= dom p by RELAT_1:89;
A41: k <= len p by A39, A40, FINSEQ_3:27;
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, A41;
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 )
A45: len q <= (len q) + 1 by NAT_1:11;
A46: k <= len q2 by A12, A38, A45, XXREAL_0:2;
A47: k in dom q2 by A37, A46, FINSEQ_3:27;
thus x9 = q2 . k by A42, A47, FUNCT_1:70; :: thesis: ( y9 = q2 . (k + 1) & q . k joins x9,y9 )
A48: k + 1 <= len q2 by A12, A38, XREAL_1:9;
A49: 1 + 1 <= k + 1 by A37, XREAL_1:9;
A50: 1 <= k + 1 by A49, XXREAL_0:2;
A51: k + 1 in dom q2 by A48, A50, FINSEQ_3:27;
thus y9 = q2 . (k + 1) by A43, A51, FUNCT_1:70; :: thesis: q . k joins x9,y9
thus q . k joins x9,y9 by A39, A44, FUNCT_1:70; :: thesis: verum

end;

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