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;

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) ) )

hence
G -VSet (rng c) = rng vs
by TARSKI:2; :: thesis: verum( ( 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 b_{1} in G -VSet (rng c) ) )

_{1} 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;

end;hereby :: thesis: ( y in rng vs implies b_{1} in G -VSet (rng c) )

assume
y in rng vs
; :: thesis: bassume
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 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; :: thesis: verum

end;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 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; :: thesis: verum

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;

end;

suppose A22:
x <= len c
; :: thesis: b_{1} 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; :: thesis: verum

end;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; :: thesis: verum

suppose A26:
x = (len c) + 1
; :: thesis: b_{1} 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; :: thesis: verum

end;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; :: thesis: verum