let G be Graph; :: thesis: for vs being FinSequence of the carrier of G
for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
vs is_vertex_seq_of c
let vs be FinSequence of the carrier of G; :: thesis: for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
vs is_vertex_seq_of c
let c be oriented Chain of G; :: thesis: ( vs is_oriented_vertex_seq_of c implies vs is_vertex_seq_of c )
assume A1: vs is_oriented_vertex_seq_of c ; :: thesis: vs is_vertex_seq_of c
then A2: len vs = (len c) + 1 by Def5;
for n being Element of NAT st 1 <= n & n <= len c holds
c . n joins vs /. n,vs /. (n + 1)

proof

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len c implies c . n joins vs /. n,vs /. (n + 1) )
assume that
A3: 1 <= n and
A4: n <= len c ; :: thesis: c . n joins vs /. n,vs /. (n + 1)
c . n orientedly_joins vs /. n,vs /. (n + 1) by A1, A3, A4, Def5;
hence c . n joins vs /. n,vs /. (n + 1) by Th1; :: thesis: verum

end;

hence vs is_vertex_seq_of c by A2, GRAPH_2:def 7; :: thesis: verum