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

proof

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;

then reconsider p = p as FinSequence of the carrier of G by FINSEQ_1:def 4;
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