let G be Graph; 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; 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; ( vs is_oriented_vertex_seq_of c implies G -TVSet (rng c) c= rng vs )
assume A1:
vs is_oriented_vertex_seq_of c
; G -TVSet (rng c) c= rng vs
then A2:
len vs = (len c) + 1
;
let y be object ; TARSKI:def 3 ( not y in G -TVSet (rng c) or y in rng vs )
assume
y in G -TVSet (rng c)
; y in rng vs
then consider v being Element of G such that
A3:
v = y
and
A4:
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
A5:
e in rng c
and
A6:
v = the Target of G . e
by A4;
consider x being object such that
A7:
x in dom c
and
A8:
e = c . x
by A5, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A7;
A9:
1 <= x
by A7, FINSEQ_3:25;
A10:
x <= len c
by A7, FINSEQ_3:25;
A11:
1 <= x + 1
by NAT_1:12;
A12:
x + 1 <= len vs
by A2, A10, XREAL_1:7;
set v1 = vs /. x;
set v2 = vs /. (x + 1);
A13:
vs /. (x + 1) = vs . (x + 1)
by A2, A10, A11, FINSEQ_4:15, XREAL_1:7;
c . x orientedly_joins vs /. x,vs /. (x + 1)
by A1, A9, A10;
then A14:
v = vs /. (x + 1)
by A6, A8;
x + 1 in dom vs
by A11, A12, FINSEQ_3:25;
hence
y in rng vs
by A3, A13, A14, FUNCT_1:def 3; verum