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 -SVSet (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 -SVSet (rng c) c= rng vs
let c be oriented Chain of G; :: thesis: ( vs is_oriented_vertex_seq_of c implies G -SVSet (rng c) c= rng vs )
assume A1:
vs is_oriented_vertex_seq_of c
; :: thesis: G -SVSet (rng c) c= rng vs
then A2:
len vs = (len c) + 1
by Def5;
G -SVSet (rng c) c= rng vs
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in G -SVSet (rng c) or y in rng vs )
assume
y in G -SVSet (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
Source of
G . e ) )
;
consider e being
Element of the
carrier' of
G such that A4:
(
e in rng c &
v = the
Source 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
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
end;
hence
G -SVSet (rng c) c= rng vs
; :: thesis: verum