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