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
G -TVSet (rng c) c= rng vs
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
G -TVSet (rng c) c= rng vs
let c be oriented Chain of G; :: thesis: ( vs is_oriented_vertex_seq_of c implies G -TVSet (rng c) c= rng vs )
assume A1: vs is_oriented_vertex_seq_of c ; :: thesis: G -TVSet (rng c) c= rng vs
then A2: len vs = (len c) + 1 by Def5;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in G -TVSet (rng c) or y in rng vs )
assume y in G -TVSet (rng c) ; :: thesis: y in rng vs
then consider v being Element of the carrier of G such that
A3: ( v = y & ex e being Element of the carrier' of G st
( e in rng c & v = the Target of G . e ) ) ;
consider e being Element of the carrier' of G such that
A4: ( e in rng c & v = the Target of G . e ) by A3;
consider x being set such that
A5: ( x in dom c & e = c . x ) by A4, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A5;
A6: ( 1 <= x & x <= len c ) by A5, FINSEQ_3:27;
then A7: ( 1 <= x + 1 & x + 1 <= len vs & x <= len vs ) by A2, NAT_1:12, XREAL_1:9;
set v1 = vs /. x;
set v2 = vs /. (x + 1);
A8: ( vs /. x = vs . x & vs /. (x + 1) = vs . (x + 1) ) by A6, A7, FINSEQ_4:24;
c . x orientedly_joins vs /. x,vs /. (x + 1) by A1, A6, Def5;
then A9: v = vs /. (x + 1) by A4, A5, Def1;
( x in dom vs & x + 1 in dom vs ) by A6, A7, FINSEQ_3:27;
hence y in rng vs by A3, A8, A9, FUNCT_1:def 5; :: thesis: verum