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 vs' being FinSequence of the carrier of (AddNewEdge v1,v2) st vs' = vs & vs is_vertex_seq_of c holds
vs' 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 vs' being FinSequence of the carrier of (AddNewEdge v1,v2) st vs' = vs & vs is_vertex_seq_of c holds
vs' is_vertex_seq_of c
let c be Chain of G; :: thesis: for vs being FinSequence of the carrier of G
for vs' being FinSequence of the carrier of (AddNewEdge v1,v2) st vs' = vs & vs is_vertex_seq_of c holds
vs' is_vertex_seq_of c
let vs be FinSequence of the carrier of G; :: thesis: for vs' being FinSequence of the carrier of (AddNewEdge v1,v2) st vs' = vs & vs is_vertex_seq_of c holds
vs' is_vertex_seq_of c
let vs' be FinSequence of the carrier of (AddNewEdge v1,v2); :: thesis: ( vs' = vs & vs is_vertex_seq_of c implies vs' is_vertex_seq_of c )
assume A1: ( vs' = vs & vs is_vertex_seq_of c ) ; :: thesis: vs' is_vertex_seq_of c
set S = the Source of G;
set T = the Target of G;
set G' = AddNewEdge v1,v2;
set S' = the Source of (AddNewEdge v1,v2);
set T' = the Target of (AddNewEdge v1,v2);
thus len vs' = (len c) + 1 by A1, GRAPH_2:def 7; :: according to GRAPH_2:def 7 :: thesis: for b₁ being Element of NAT holds
( not 1 <= b₁ or not b₁ <= len c or c . b₁ joins vs' /. b₁,vs' /. (b₁ + 1) )
A2: the carrier of G = the carrier of (AddNewEdge v1,v2) by Def7;
let n be Element of NAT ; :: thesis: ( not 1 <= n or not n <= len c or c . n joins vs' /. n,vs' /. (n + 1) )
assume A3: ( 1 <= n & n <= len c ) ; :: thesis: c . n joins vs' /. n,vs' /. (n + 1)
then A4: c . n joins vs /. n,vs /. (n + 1) by A1, GRAPH_2:def 7;
set v = c . n;
set x = vs /. n;
set y = vs /. (n + 1);
A5: ( ( 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 ) ) by A4, GRAPH_1:def 10;
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:27;
then c . n in rng c by FUNCT_1:def 5;
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, Th40;
hence c . n joins vs' /. n,vs' /. (n + 1) by A1, A2, A5, GRAPH_1:def 10; :: thesis: verum