let G be Graph; 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; 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; ( 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
; G -VSet (rng c) = rng vs
A3:
len vs = (len c) + 1
by A2;
now for y being object holds
( ( y in G -VSet (rng c) implies y in rng vs ) & ( y in rng vs implies y in G -VSet (rng c) ) )let y be
object ;
( ( y in G -VSet (rng c) implies y in rng vs ) & ( y in rng vs implies b1 in G -VSet (rng c) ) )hereby ( y in rng vs implies b1 in G -VSet (rng c) )
assume
y in G -VSet (rng c)
;
y in rng vsthen consider v being
Element of
G such that A4:
v = y
and A5:
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 A6:
e in rng c
and A7:
(
v = the
Source of
G . e or
v = the
Target of
G . e )
by A5;
consider x being
object such that A8:
x in dom c
and A9:
e = c . x
by A6, FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A8;
A10:
1
<= x + 1
by NAT_1:12;
set v2 =
vs /. (x + 1);
set v1 =
vs /. x;
A11:
x <= len c
by A8, FINSEQ_3:25;
then A12:
x + 1
in dom vs
by A10, FINSEQ_3:25, A3, XREAL_1:7;
A13:
1
<= x
by A8, FINSEQ_3:25;
then
c . x joins vs /. x,
vs /. (x + 1)
by A2, A11;
then A14:
(
v = vs /. x or
v = vs /. (x + 1) )
by A7, A9;
A15:
x <= len vs
by A3, A11, NAT_1:12;
then A16:
vs /. x = vs . x
by A13, FINSEQ_4:15;
A17:
x in dom vs
by A13, A15, FINSEQ_3:25;
vs /. (x + 1) = vs . (x + 1)
by A3, A11, A10, FINSEQ_4:15, XREAL_1:7;
hence
y in rng vs
by A4, A16, A14, A17, A12, FUNCT_1:def 3;
verum
end; assume
y in rng vs
;
b1 in G -VSet (rng c)then consider x being
object such that A18:
x in dom vs
and A19:
y = vs . x
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A18;
A20:
1
<= x
by A18, FINSEQ_3:25;
A21:
x <= len vs
by A18, FINSEQ_3:25;
per cases
( x <= len c or x = (len c) + 1 )
by A3, A21, NAT_1:8;
suppose A22:
x <= len c
;
b1 in G -VSet (rng c)then
x in dom c
by A20, FINSEQ_3:25;
then A23:
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 A23;
x in dom c
by A20, A22, FINSEQ_3:25;
then A24:
e in rng c
by FUNCT_1:def 3;
set v2 =
vs /. (x + 1);
set v1 =
vs /. x;
c . x joins vs /. x,
vs /. (x + 1)
by A2, A20, A22;
then A25:
( (
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 ) )
;
vs /. x = vs . x
by A20, A21, FINSEQ_4:15;
hence
y in G -VSet (rng c)
by A19, A25, A24;
verum end; suppose A26:
x = (len c) + 1
;
b1 in G -VSet (rng c)set l =
len c;
A27:
rng c c= the
carrier' of
G
by FINSEQ_1:def 4;
0 + 1
= 1
;
then A28:
1
<= len c
by A1, NAT_1:13;
then
len c in dom c
by FINSEQ_3:25;
then
c . (len c) in rng c
by FUNCT_1:def 3;
then reconsider e =
c . (len c) as
Element of the
carrier' of
G by A27;
set v2 =
vs /. ((len c) + 1);
set v1 =
vs /. (len c);
len c in dom c
by A28, FINSEQ_3:25;
then A29:
e in rng c
by FUNCT_1:def 3;
c . (len c) joins vs /. (len c),
vs /. ((len c) + 1)
by A2, A28;
then A30:
( (
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 ) )
;
vs /. ((len c) + 1) = vs . ((len c) + 1)
by A3, A20, A26, FINSEQ_4:15;
hence
y in G -VSet (rng c)
by A19, A26, A30, A29;
verum end; end;
hence
G -VSet (rng c) = rng vs
by TARSKI:2; verum