let G be Graph; for vs being FinSequence of the carrier of G
for c being oriented Chain of G st c <> {} & vs is_oriented_vertex_seq_of c holds
rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c))
let vs be FinSequence of the carrier of G; for c being oriented Chain of G st c <> {} & vs is_oriented_vertex_seq_of c holds
rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c))
let c be oriented Chain of G; ( c <> {} & vs is_oriented_vertex_seq_of c implies rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c)) )
assume that
A1:
c <> {}
and
A2:
vs is_oriented_vertex_seq_of c
; rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c))
A3:
len vs = (len c) + 1
by A2;
let y be object ; TARSKI:def 3 ( not y in rng vs or y in (G -SVSet (rng c)) \/ (G -TVSet (rng c)) )
assume
y in rng vs
; y in (G -SVSet (rng c)) \/ (G -TVSet (rng c))
then consider x being object such that
A4:
x in dom vs
and
A5:
y = vs . x
by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A4;
A6:
1 <= x
by A4, FINSEQ_3:25;
A7:
x <= len vs
by A4, FINSEQ_3:25;
per cases
( x <= len c or x = (len c) + 1 )
by A3, A7, NAT_1:8;
suppose A8:
x <= len c
;
y in (G -SVSet (rng c)) \/ (G -TVSet (rng c))then
x in dom c
by A6, FINSEQ_3:25;
then A9:
c . x in rng c
by FUNCT_1:def 3;
rng c c= the
carrier' of
G
by FINSEQ_1:def 4;
then reconsider e =
c . x as
Element of the
carrier' of
G by A9;
set v1 =
vs /. x;
set v2 =
vs /. (x + 1);
A10:
vs /. x = vs . x
by A6, A7, FINSEQ_4:15;
c . x orientedly_joins vs /. x,
vs /. (x + 1)
by A2, A6, A8;
then A11:
vs /. x = the
Source of
G . e
;
x in dom c
by A6, A8, FINSEQ_3:25;
then
e in rng c
by FUNCT_1:def 3;
then
y in G -SVSet (rng c)
by A5, A10, A11;
hence
y in (G -SVSet (rng c)) \/ (G -TVSet (rng c))
by XBOOLE_0:def 3;
verum end; suppose A12:
x = (len c) + 1
;
y in (G -SVSet (rng c)) \/ (G -TVSet (rng c))set l =
len c;
0 + 1
= 1
;
then A13:
1
<= len c
by A1, NAT_1:13;
then
len c in dom c
by FINSEQ_3:25;
then A14:
c . (len c) in rng c
by FUNCT_1:def 3;
rng c c= the
carrier' of
G
by FINSEQ_1:def 4;
then reconsider e =
c . (len c) as
Element of the
carrier' of
G by A14;
set v1 =
vs /. (len c);
set v2 =
vs /. ((len c) + 1);
A15:
vs /. ((len c) + 1) = vs . ((len c) + 1)
by A3, A6, A12, FINSEQ_4:15;
c . (len c) orientedly_joins vs /. (len c),
vs /. ((len c) + 1)
by A2, A13;
then A16:
vs /. ((len c) + 1) = the
Target of
G . e
;
len c in dom c
by A13, FINSEQ_3:25;
then
e in rng c
by FUNCT_1:def 3;
then
y in G -TVSet (rng c)
by A5, A12, A15, A16;
hence
y in (G -SVSet (rng c)) \/ (G -TVSet (rng c))
by XBOOLE_0:def 3;
verum end;