let G be Graph; for v1, v2 being Vertex of G
for vs being FinSequence of the carrier of G
for p9 being Path of AddNewEdge (v1,v2)
for vs9 being FinSequence of the carrier of (AddNewEdge (v1,v2)) st not the carrier' of G in rng p9 & vs = vs9 & vs9 is_vertex_seq_of p9 holds
vs is_vertex_seq_of p9
let v1, v2 be Vertex of G; for vs being FinSequence of the carrier of G
for p9 being Path of AddNewEdge (v1,v2)
for vs9 being FinSequence of the carrier of (AddNewEdge (v1,v2)) st not the carrier' of G in rng p9 & vs = vs9 & vs9 is_vertex_seq_of p9 holds
vs is_vertex_seq_of p9
let vs be FinSequence of the carrier of G; for p9 being Path of AddNewEdge (v1,v2)
for vs9 being FinSequence of the carrier of (AddNewEdge (v1,v2)) st not the carrier' of G in rng p9 & vs = vs9 & vs9 is_vertex_seq_of p9 holds
vs is_vertex_seq_of p9
let p9 be Path of AddNewEdge (v1,v2); for vs9 being FinSequence of the carrier of (AddNewEdge (v1,v2)) st not the carrier' of G in rng p9 & vs = vs9 & vs9 is_vertex_seq_of p9 holds
vs is_vertex_seq_of p9
let vs9 be FinSequence of the carrier of (AddNewEdge (v1,v2)); ( not the carrier' of G in rng p9 & vs = vs9 & vs9 is_vertex_seq_of p9 implies vs is_vertex_seq_of p9 )
set G9 = AddNewEdge (v1,v2);
set S = the Source of G;
set T = the Target of G;
set E = the carrier' of G;
set S9 = the Source of (AddNewEdge (v1,v2));
set T9 = the Target of (AddNewEdge (v1,v2));
the carrier' of (AddNewEdge (v1,v2)) = the carrier' of G \/ { the carrier' of G}
by Def7;
then A1:
rng p9 c= the carrier' of G \/ { the carrier' of G}
by FINSEQ_1:def 4;
assume A2:
not the carrier' of G in rng p9
; ( not vs = vs9 or not vs9 is_vertex_seq_of p9 or vs is_vertex_seq_of p9 )
A3:
rng p9 c= the carrier' of G
assume that
A5:
vs = vs9
and
A6:
vs9 is_vertex_seq_of p9
; vs is_vertex_seq_of p9
thus
vs is_vertex_seq_of p9
verumproof
thus A7:
len vs = (len p9) + 1
by A5, A6;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len p9 or p9 . b1 joins vs /. b1,vs /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len p9 or p9 . n joins vs /. n,vs /. (n + 1) )
assume that A8:
1
<= n
and A9:
n <= len p9
;
p9 . n joins vs /. n,vs /. (n + 1)
set e =
p9 . n;
reconsider vn9 =
vs9 /. n,
vn19 =
vs9 /. (n + 1) as
Vertex of
(AddNewEdge (v1,v2)) ;
p9 . n joins vs9 /. n,
vs9 /. (n + 1)
by A6, A8, A9;
then A10:
( ( the
Source of
(AddNewEdge (v1,v2)) . (p9 . n) = vn9 & the
Target of
(AddNewEdge (v1,v2)) . (p9 . n) = vn19 ) or ( the
Source of
(AddNewEdge (v1,v2)) . (p9 . n) = vn19 & the
Target of
(AddNewEdge (v1,v2)) . (p9 . n) = vn9 ) )
;
reconsider vn =
vs /. n,
vn1 =
vs /. (n + 1) as
Vertex of
G ;
( 1
<= n + 1 &
n + 1
<= len vs )
by A7, A9, NAT_1:11, XREAL_1:6;
then A11:
n + 1
in dom vs
by FINSEQ_3:25;
then A12:
vn1 =
vs . (n + 1)
by PARTFUN1:def 6
.=
vn19
by A5, A11, PARTFUN1:def 6
;
n in dom p9
by A8, A9, FINSEQ_3:25;
then
p9 . n in rng p9
by FUNCT_1:def 3;
then A13:
( the
Source of
(AddNewEdge (v1,v2)) . (p9 . n) = the
Source of
G . (p9 . n) & the
Target of
(AddNewEdge (v1,v2)) . (p9 . n) = the
Target of
G . (p9 . n) )
by A3, Th35;
len p9 <= len vs
by A7, NAT_1:11;
then
n <= len vs
by A9, XXREAL_0:2;
then A14:
n in dom vs
by A8, FINSEQ_3:25;
then vn =
vs . n
by PARTFUN1:def 6
.=
vn9
by A5, A14, PARTFUN1:def 6
;
hence
p9 . n joins vs /. n,
vs /. (n + 1)
by A10, A13, A12;
verum
end;