let G be Graph; :: thesis: for c being Chain of G ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c

let c be Chain of G; :: thesis: ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c

consider p being FinSequence such that

A1: len p = (len c) + 1 and

A2: for n being Nat st 1 <= n & n <= len p holds

p . n in the carrier of G and

A3: for n being Nat st 1 <= n & n <= len c holds

ex v1, v2 being Element of G st

( v1 = p . n & v2 = p . (n + 1) & c . n joins v1,v2 ) by GRAPH_1:def 14;

rng p c= the carrier of G

take p ; :: thesis: p is_vertex_seq_of c

thus len p = (len c) + 1 by A1; :: according to GRAPH_2:def 2 :: thesis: for n being Nat st 1 <= n & n <= len c holds

c . n joins p /. n,p /. (n + 1)

let n be Nat; :: thesis: ( 1 <= n & n <= len c implies c . n joins p /. n,p /. (n + 1) )

assume that

A7: 1 <= n and

A8: n <= len c ; :: thesis: c . n joins p /. n,p /. (n + 1)

A9: n <= len p by A1, A8, NAT_1:12;

1 <= n + 1 by NAT_1:12;

then A10: p /. (n + 1) = p . (n + 1) by A1, A8, FINSEQ_4:15, XREAL_1:7;

ex v1, v2 being Element of G st

( v1 = p . n & v2 = p . (n + 1) & c . n joins v1,v2 ) by A3, A7, A8;

hence c . n joins p /. n,p /. (n + 1) by A7, A9, A10, FINSEQ_4:15; :: thesis: verum

let c be Chain of G; :: thesis: ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c

consider p being FinSequence such that

A1: len p = (len c) + 1 and

A2: for n being Nat st 1 <= n & n <= len p holds

p . n in the carrier of G and

A3: for n being Nat st 1 <= n & n <= len c holds

ex v1, v2 being Element of G st

( v1 = p . n & v2 = p . (n + 1) & c . n joins v1,v2 ) by GRAPH_1:def 14;

rng p c= the carrier of G

proof

then reconsider p = p as FinSequence of the carrier of G by FINSEQ_1:def 4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in the carrier of G )

assume y in rng p ; :: thesis: y in the carrier of G

then consider x being object such that

A4: x in dom p and

A5: y = p . x by FUNCT_1:def 3;

reconsider n = x as Element of NAT by A4;

A6: n <= len p by A4, FINSEQ_3:25;

1 <= n by A4, FINSEQ_3:25;

hence y in the carrier of G by A2, A5, A6; :: thesis: verum

end;assume y in rng p ; :: thesis: y in the carrier of G

then consider x being object such that

A4: x in dom p and

A5: y = p . x by FUNCT_1:def 3;

reconsider n = x as Element of NAT by A4;

A6: n <= len p by A4, FINSEQ_3:25;

1 <= n by A4, FINSEQ_3:25;

hence y in the carrier of G by A2, A5, A6; :: thesis: verum

take p ; :: thesis: p is_vertex_seq_of c

thus len p = (len c) + 1 by A1; :: according to GRAPH_2:def 2 :: thesis: for n being Nat st 1 <= n & n <= len c holds

c . n joins p /. n,p /. (n + 1)

let n be Nat; :: thesis: ( 1 <= n & n <= len c implies c . n joins p /. n,p /. (n + 1) )

assume that

A7: 1 <= n and

A8: n <= len c ; :: thesis: c . n joins p /. n,p /. (n + 1)

A9: n <= len p by A1, A8, NAT_1:12;

1 <= n + 1 by NAT_1:12;

then A10: p /. (n + 1) = p . (n + 1) by A1, A8, FINSEQ_4:15, XREAL_1:7;

ex v1, v2 being Element of G st

( v1 = p . n & v2 = p . (n + 1) & c . n joins v1,v2 ) by A3, A7, A8;

hence c . n joins p /. n,p /. (n + 1) by A7, A9, A10, FINSEQ_4:15; :: thesis: verum