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;
now :: thesis: 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 ; :: 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 vs
then 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 ;
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 ;
then A12: x + 1 in dom vs by ;
A13: 1 <= x by ;
then c . x joins vs /. x,vs /. (x + 1) by ;
then A14: ( v = vs /. x or v = vs /. (x + 1) ) by A7, A9;
A15: x <= len vs by ;
then A16: vs /. x = vs . x by ;
A17: x in dom vs by ;
vs /. (x + 1) = vs . (x + 1) by ;
hence y in rng vs by ; :: thesis: verum
end;
assume y in rng vs ; :: thesis: 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 ;
A21: x <= len vs by ;
per cases ( x <= len c or x = (len c) + 1 ) by ;
suppose A22: x <= len c ; :: thesis: b1 in G -VSet (rng c)
then x in dom c by ;
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 ;
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 ;
hence y in G -VSet (rng c) by ; :: thesis: verum
end;
suppose A26: x = (len c) + 1 ; :: thesis: 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 ;
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 ;
then A29: e in rng c by FUNCT_1:def 3;
c . (len c) joins vs /. (len c),vs /. ((len c) + 1) by ;
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 ;
hence y in G -VSet (rng c) by A19, A26, A30, A29; :: thesis: verum
end;
end;
end;
hence G -VSet (rng c) = rng vs by TARSKI:2; :: thesis: verum