let G be Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( c <> {} & vs is_oriented_vertex_seq_of c implies rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c)) )
assume A1:
( c <> {} & vs is_oriented_vertex_seq_of c )
; :: thesis: rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c))
then A2:
len vs = (len c) + 1
by Def5;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng vs or y in (G -SVSet (rng c)) \/ (G -TVSet (rng c)) )
assume
y in rng vs
; :: thesis: y in (G -SVSet (rng c)) \/ (G -TVSet (rng c))
then consider x being set such that
A3:
( x in dom vs & y = vs . x )
by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A3;
A4:
( 1 <= x & x <= len vs )
by A3, FINSEQ_3:27;
per cases
( x <= len c or x = (len c) + 1 )
by A2, A4, NAT_1:8;
suppose A5:
x <= len c
;
:: thesis: y in (G -SVSet (rng c)) \/ (G -TVSet (rng c))then A6:
( 1
<= x + 1 &
x + 1
<= len vs &
x <= len vs )
by A2, NAT_1:12, XREAL_1:9;
x in dom c
by A4, A5, FINSEQ_3:27;
then
(
c . x in rng c &
rng c c= the
carrier' of
G )
by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider e =
c . x as
Element of the
carrier' of
G ;
set v1 =
vs /. x;
set v2 =
vs /. (x + 1);
A7:
(
vs /. x = vs . x &
vs /. (x + 1) = vs . (x + 1) )
by A4, A6, FINSEQ_4:24;
c . x orientedly_joins vs /. x,
vs /. (x + 1)
by A1, A4, A5, Def5;
then A8:
(
vs /. x = the
Source of
G . e &
vs /. (x + 1) = the
Target of
G . e )
by Def1;
x in dom c
by A4, A5, FINSEQ_3:27;
then
e in rng c
by FUNCT_1:def 5;
then
y in G -SVSet (rng c)
by A3, A7, A8;
hence
y in (G -SVSet (rng c)) \/ (G -TVSet (rng c))
by XBOOLE_0:def 3;
:: thesis: verum end; suppose A9:
x = (len c) + 1
;
:: thesis: y in (G -SVSet (rng c)) \/ (G -TVSet (rng c))set l =
len c;
len c <> 0
by A1;
then
(
0 < len c &
0 + 1
= 1 )
;
then A10:
( 1
<= len c &
len c <= (len c) + 1 )
by NAT_1:13;
then
len c in dom c
by FINSEQ_3:27;
then
(
c . (len c) in rng c &
rng c c= the
carrier' of
G )
by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider e =
c . (len c) as
Element of the
carrier' of
G ;
set v1 =
vs /. (len c);
set v2 =
vs /. ((len c) + 1);
A11:
(
vs /. (len c) = vs . (len c) &
vs /. ((len c) + 1) = vs . ((len c) + 1) )
by A2, A4, A9, A10, FINSEQ_4:24;
c . (len c) orientedly_joins vs /. (len c),
vs /. ((len c) + 1)
by A1, A10, Def5;
then A12:
(
vs /. (len c) = the
Source of
G . e &
vs /. ((len c) + 1) = the
Target of
G . e )
by Def1;
len c in dom c
by A10, FINSEQ_3:27;
then
e in rng c
by FUNCT_1:def 5;
then
y in G -TVSet (rng c)
by A3, A9, A11, A12;
hence
y in (G -SVSet (rng c)) \/ (G -TVSet (rng c))
by XBOOLE_0:def 3;
:: thesis: verum end;