let G be Graph; :: thesis: for v1, v2 being Vertex of G
for c being Chain of G
for vs being FinSequence of the carrier of G
for vs9 being FinSequence of the carrier of (AddNewEdge (v1,v2)) st vs9 = vs & vs is_vertex_seq_of c holds
vs9 is_vertex_seq_of c
let v1, v2 be Vertex of G; :: thesis: for c being Chain of G
for vs being FinSequence of the carrier of G
for vs9 being FinSequence of the carrier of (AddNewEdge (v1,v2)) st vs9 = vs & vs is_vertex_seq_of c holds
vs9 is_vertex_seq_of c
let c be Chain of G; :: thesis: for vs being FinSequence of the carrier of G
for vs9 being FinSequence of the carrier of (AddNewEdge (v1,v2)) st vs9 = vs & vs is_vertex_seq_of c holds
vs9 is_vertex_seq_of c
let vs be FinSequence of the carrier of G; :: thesis: for vs9 being FinSequence of the carrier of (AddNewEdge (v1,v2)) st vs9 = vs & vs is_vertex_seq_of c holds
vs9 is_vertex_seq_of c
let vs9 be FinSequence of the carrier of (AddNewEdge (v1,v2)); :: thesis: ( vs9 = vs & vs is_vertex_seq_of c implies vs9 is_vertex_seq_of c )
assume that
A1: vs9 = vs and
A2: vs is_vertex_seq_of c ; :: thesis: vs9 is_vertex_seq_of c
thus len vs9 = (len c) + 1 by A1, A2; :: according to GRAPH_2:def 2 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len c or c . b₁ joins vs9 /. b₁,vs9 /. (b₁ + 1) )
let n be Nat; :: thesis: ( not 1 <= n or not n <= len c or c . n joins vs9 /. n,vs9 /. (n + 1) )
set T = the Target of G;
set S = the Source of G;
set v = c . n;
set x = vs /. n;
set y = vs /. (n + 1);
assume A3: ( 1 <= n & n <= len c ) ; :: thesis: c . n joins vs9 /. n,vs9 /. (n + 1)
then c . n joins vs /. n,vs /. (n + 1) by A2;
then A4: ( ( the Source of G . (c . n) = vs /. n & the Target of G . (c . n) = vs /. (n + 1) ) or ( the Source of G . (c . n) = vs /. (n + 1) & the Target of G . (c . n) = vs /. n ) ) ;
set G9 = AddNewEdge (v1,v2);
set S9 = the Source of (AddNewEdge (v1,v2));
set T9 = the Target of (AddNewEdge (v1,v2));
A5: the carrier of G = the carrier of (AddNewEdge (v1,v2)) by Def7;
c is FinSequence of the carrier' of G by MSSCYC_1:def 1;
then A6: rng c c= the carrier' of G by FINSEQ_1:def 4;
n in dom c by A3, FINSEQ_3:25;
then c . n in rng c by FUNCT_1:def 3;
then ( the Source of (AddNewEdge (v1,v2)) . (c . n) = the Source of G . (c . n) & the Target of G . (c . n) = the Target of (AddNewEdge (v1,v2)) . (c . n) ) by A6, Th35;
hence c . n joins vs9 /. n,vs9 /. (n + 1) by A1, A5, A4; :: thesis: verum