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 & ( for n being Element of NAT st 1 <= n & n <= len p holds
p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len c holds
ex v1, v2 being Element of the carrier of G st
( v1 = p . n & v2 = p . (n + 1) & c . n joins v1,v2 ) ) ) by GRAPH_1:def 12;
rng p c= the carrier of G

proof

let y be set ; :: 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 set such that
A2: ( x in dom p & y = p . x ) by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A2;
( 1 <= n & n <= len p ) by A2, FINSEQ_3:27;
hence y in the carrier of G by A1, A2; :: 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 7 :: thesis: for n being Element of NAT st 1 <= n & n <= len c holds
c . n joins p /. n,p /. (n + 1)
let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len c implies c . n joins p /. n,p /. (n + 1) )
assume that
A3: 1 <= n and
A4: n <= len c ; :: thesis: c . n joins p /. n,p /. (n + 1)
consider v1, v2 being Element of the carrier of G such that
A5: ( v1 = p . n & v2 = p . (n + 1) & c . n joins v1,v2 ) by A1, A3, A4;
A6: ( 1 <= n + 1 & len c <= (len c) + 1 & n + 1 <= (len c) + 1 ) by A4, NAT_1:12, XREAL_1:9;
n <= len p by A1, A4, NAT_1:12;
then ( p /. n = p . n & p /. (n + 1) = p . (n + 1) ) by A1, A3, A6, FINSEQ_4:24;
hence c . n joins p /. n,p /. (n + 1) by A5; :: thesis: verum