let G be Graph; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: 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)); :: thesis: ( 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 ; :: thesis: ( 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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p9 or x in the carrier' of G )
assume A4: x in rng p9 ; :: thesis: x in the carrier' of G
then ( x in the carrier' of G or x in { the carrier' of G} ) by A1, XBOOLE_0:def 3;
hence x in the carrier' of G by A2, A4, TARSKI:def 1; :: thesis: verum

end;

assume that
A5: vs = vs9 and
A6: vs9 is_vertex_seq_of p9 ; :: thesis: vs is_vertex_seq_of p9
thus vs is_vertex_seq_of p9 :: thesis: verum

proof

thus A7: len vs = (len p9) + 1 by A5, A6; :: according to GRAPH_2:def 2 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len p9 or p9 . b₁ joins vs /. b₁,vs /. (b₁ + 1) )
let n be Nat; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;