let G be Graph; :: thesis: for vs being FinSequence of the carrier of G
for c being Chain of G st c <> {} & vs is_vertex_seq_of c holds
G -VSet (rng c) = rng vs
let vs be FinSequence of the carrier of G; :: thesis: for c being Chain of G st c <> {} & vs is_vertex_seq_of c holds
G -VSet (rng c) = rng vs
let c be Chain of G; :: thesis: ( c <> {} & vs is_vertex_seq_of c implies G -VSet (rng c) = rng vs )
assume that
A1:
c <> {}
and
A2:
vs is_vertex_seq_of c
; :: thesis: G -VSet (rng c) = rng vs
A3:
len vs = (len c) + 1
by A2, Def7;
now let y be
set ;
:: thesis: ( ( y in G -VSet (rng c) implies y in rng vs ) & ( y in rng vs implies b1 in G -VSet (rng c) ) )hereby :: thesis: ( y in rng vs implies b1 in G -VSet (rng c) )
assume
y in G -VSet (rng c)
;
:: thesis: y in rng vsthen consider v being
Element of the
carrier of
G such that A4:
(
v = y & ex
e being
Element of the
carrier' of
G st
(
e in rng c & (
v = the
Source of
G . e or
v = the
Target of
G . e ) ) )
;
consider e being
Element of the
carrier' of
G such that A5:
(
e in rng c & (
v = the
Source of
G . e or
v = the
Target of
G . e ) )
by A4;
consider x being
set such that A6:
(
x in dom c &
e = c . x )
by A5, FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A6;
A7:
( 1
<= x &
x <= len c )
by A6, FINSEQ_3:27;
then A8:
( 1
<= x + 1 &
x + 1
<= len vs &
x <= len vs )
by A3, NAT_1:12, XREAL_1:9;
set v1 =
vs /. x;
set v2 =
vs /. (x + 1);
A9:
(
vs /. x = vs . x &
vs /. (x + 1) = vs . (x + 1) )
by A7, A8, FINSEQ_4:24;
c . x joins vs /. x,
vs /. (x + 1)
by A2, A7, Def7;
then A10:
(
v = vs /. x or
v = vs /. (x + 1) )
by A5, A6, GRAPH_1:def 10;
(
x in dom vs &
x + 1
in dom vs )
by A7, A8, FINSEQ_3:27;
hence
y in rng vs
by A4, A9, A10, FUNCT_1:def 5;
:: thesis: verum
end; assume
y in rng vs
;
:: thesis: b1 in G -VSet (rng c)then consider x being
set such that A11:
(
x in dom vs &
y = vs . x )
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A11;
A12:
( 1
<= x &
x <= len vs )
by A11, FINSEQ_3:27;
per cases
( x <= len c or x = (len c) + 1 )
by A3, A12, NAT_1:8;
suppose A13:
x <= len c
;
:: thesis: b1 in G -VSet (rng c)then A14:
( 1
<= x + 1 &
x + 1
<= len vs &
x <= len vs )
by A3, NAT_1:12, XREAL_1:9;
x in dom c
by A12, A13, 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);
A15:
(
vs /. x = vs . x &
vs /. (x + 1) = vs . (x + 1) )
by A12, A14, FINSEQ_4:24;
c . x joins vs /. x,
vs /. (x + 1)
by A2, A12, A13, Def7;
then A16:
( (
vs /. x = the
Source of
G . e &
vs /. (x + 1) = the
Target of
G . e ) or (
vs /. (x + 1) = the
Source of
G . e &
vs /. x = the
Target of
G . e ) )
by GRAPH_1:def 10;
x in dom c
by A12, A13, FINSEQ_3:27;
then
e in rng c
by FUNCT_1:def 5;
hence
y in G -VSet (rng c)
by A11, A15, A16;
:: thesis: verum end; suppose A17:
x = (len c) + 1
;
:: thesis: b1 in G -VSet (rng c)set l =
len c;
len c <> 0
by A1;
then
(
0 < len c &
0 + 1
= 1 )
;
then A18:
( 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);
A19:
(
vs /. (len c) = vs . (len c) &
vs /. ((len c) + 1) = vs . ((len c) + 1) )
by A3, A12, A17, A18, FINSEQ_4:24;
c . (len c) joins vs /. (len c),
vs /. ((len c) + 1)
by A2, A18, Def7;
then A20:
( (
vs /. (len c) = the
Source of
G . e &
vs /. ((len c) + 1) = the
Target of
G . e ) or (
vs /. ((len c) + 1) = the
Source of
G . e &
vs /. (len c) = the
Target of
G . e ) )
by GRAPH_1:def 10;
len c in dom c
by A18, FINSEQ_3:27;
then
e in rng c
by FUNCT_1:def 5;
hence
y in G -VSet (rng c)
by A11, A17, A19, A20;
:: thesis: verum end; end;
hence
G -VSet (rng c) = rng vs
by TARSKI:2; :: thesis: verum