let G be Graph; :: thesis: for v1, v2 being Vertex of G
for vs being FinSequence of the carrier of G
for p' being Path of AddNewEdge v1,v2
for vs' being FinSequence of the carrier of (AddNewEdge v1,v2) st not the carrier' of G in rng p' & vs = vs' & vs' is_vertex_seq_of p' holds
vs is_vertex_seq_of p'
let v1, v2 be Vertex of G; :: thesis: for vs being FinSequence of the carrier of G
for p' being Path of AddNewEdge v1,v2
for vs' being FinSequence of the carrier of (AddNewEdge v1,v2) st not the carrier' of G in rng p' & vs = vs' & vs' is_vertex_seq_of p' holds
vs is_vertex_seq_of p'
let vs be FinSequence of the carrier of G; :: thesis: for p' being Path of AddNewEdge v1,v2
for vs' being FinSequence of the carrier of (AddNewEdge v1,v2) st not the carrier' of G in rng p' & vs = vs' & vs' is_vertex_seq_of p' holds
vs is_vertex_seq_of p'
let p' be Path of AddNewEdge v1,v2; :: thesis: for vs' being FinSequence of the carrier of (AddNewEdge v1,v2) st not the carrier' of G in rng p' & vs = vs' & vs' is_vertex_seq_of p' holds
vs is_vertex_seq_of p'
let vs' be FinSequence of the carrier of (AddNewEdge v1,v2); :: thesis: ( not the carrier' of G in rng p' & vs = vs' & vs' is_vertex_seq_of p' implies vs is_vertex_seq_of p' )
set G' = AddNewEdge v1,v2;
assume A1:
not the carrier' of G in rng p'
; :: thesis: ( not vs = vs' or not vs' is_vertex_seq_of p' or vs is_vertex_seq_of p' )
assume A2:
( vs = vs' & vs' is_vertex_seq_of p' )
; :: thesis: vs is_vertex_seq_of p'
set S = the Source of G;
set T = the Target of G;
set E = the carrier' of G;
set S' = the Source of (AddNewEdge v1,v2);
set T' = the Target of (AddNewEdge v1,v2);
the carrier' of (AddNewEdge v1,v2) = the carrier' of G \/ {the carrier' of G}
by Def7;
then A3:
rng p' c= the carrier' of G \/ {the carrier' of G}
by FINSEQ_1:def 4;
A4:
rng p' c= the carrier' of G
thus
vs is_vertex_seq_of p'
:: thesis: verumproof
thus A6:
len vs = (len p') + 1
by A2, GRAPH_2:def 7;
:: according to GRAPH_2:def 7 :: thesis: for b1 being Element of NAT holds
( not 1 <= b1 or not b1 <= len p' or p' . b1 joins vs /. b1,vs /. (b1 + 1) )
let n be
Element of
NAT ;
:: thesis: ( not 1 <= n or not n <= len p' or p' . n joins vs /. n,vs /. (n + 1) )
assume A7:
( 1
<= n &
n <= len p' )
;
:: thesis: p' . n joins vs /. n,vs /. (n + 1)
then A8:
p' . n joins vs' /. n,
vs' /. (n + 1)
by A2, GRAPH_2:def 7;
reconsider vn' =
vs' /. n,
vn1' =
vs' /. (n + 1) as
Vertex of
(AddNewEdge v1,v2) ;
set e =
p' . n;
A9:
( ( the
Source of
(AddNewEdge v1,v2) . (p' . n) = vn' & the
Target of
(AddNewEdge v1,v2) . (p' . n) = vn1' ) or ( the
Source of
(AddNewEdge v1,v2) . (p' . n) = vn1' & the
Target of
(AddNewEdge v1,v2) . (p' . n) = vn' ) )
by A8, GRAPH_1:def 10;
n in dom p'
by A7, FINSEQ_3:27;
then
p' . n in rng p'
by FUNCT_1:def 5;
then A10:
( the
Source of
(AddNewEdge v1,v2) . (p' . n) = the
Source of
G . (p' . n) & the
Target of
(AddNewEdge v1,v2) . (p' . n) = the
Target of
G . (p' . n) )
by A4, Th40;
reconsider vn =
vs /. n,
vn1 =
vs /. (n + 1) as
Vertex of
G ;
len p' <= len vs
by A6, NAT_1:11;
then
n <= len vs
by A7, XXREAL_0:2;
then A11:
n in dom vs
by A7, FINSEQ_3:27;
then A12:
vn =
vs . n
by PARTFUN1:def 8
.=
vn'
by A2, A11, PARTFUN1:def 8
;
( 1
<= n + 1 &
n + 1
<= len vs )
by A6, A7, NAT_1:11, XREAL_1:8;
then A13:
n + 1
in dom vs
by FINSEQ_3:27;
then vn1 =
vs . (n + 1)
by PARTFUN1:def 8
.=
vn1'
by A2, A13, PARTFUN1:def 8
;
hence
p' . n joins vs /. n,
vs /. (n + 1)
by A9, A10, A12, GRAPH_1:def 10;
:: thesis: verum
end;