let G be Graph; :: thesis: for v1, v2 being Vertex of G
for p' being Path of st not the carrier' of G in rng p' holds
p' is Path of
let v1, v2 be Vertex of G; :: thesis: for p' being Path of st not the carrier' of G in rng p' holds
p' is Path of
let p' be Path of ; :: thesis: ( not the carrier' of G in rng p' implies p' is Path of )
set G' = AddNewEdge v1,v2;
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 A1: rng p' c= the carrier' of G \/ {the carrier' of G} by FINSEQ_1:def 4;
assume A2: not the carrier' of G in rng p' ; :: thesis: p' is Path of
A3: rng p' c= the carrier' of G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p' or x in the carrier' of G )
assume A4: x in rng p' ; :: 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;

p' is Chain of G

proof

thus p' is FinSequence of the carrier' of G by A3, FINSEQ_1:def 4; :: according to MSSCYC_1:def 1 :: thesis: ex b₁ being FinSequence of the carrier of G st b₁ is_vertex_seq_of p'
consider vs' being FinSequence of the carrier of (AddNewEdge v1,v2) such that
A5: vs' is_vertex_seq_of p' by MSSCYC_1:def 1;
reconsider vs = vs' as FinSequence of the carrier of G by Def7;
take vs ; :: thesis: vs is_vertex_seq_of p'
thus vs is_vertex_seq_of p' :: thesis: verum

proof

thus A6: len vs = (len p') + 1 by A5, 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 p' or p' . b₁ joins vs /. b₁,vs /. (b₁ + 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 that
A7: 1 <= n and
A8: n <= len p' ; :: thesis: p' . n joins vs /. n,vs /. (n + 1)
set e = p' . n;
reconsider vn' = vs' /. n, vn1' = vs' /. (n + 1) as Vertex of (AddNewEdge v1,v2) ;
p' . n joins vs' /. n,vs' /. (n + 1) by A5, A7, A8, GRAPH_2:def 7;
then 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 GRAPH_1:def 10;
reconsider vn = vs /. n, vn1 = vs /. (n + 1) as Vertex of G ;
( 1 <= n + 1 & n + 1 <= len vs ) by A6, A8, NAT_1:11, XREAL_1:8;
then A10: n + 1 in dom vs by FINSEQ_3:27;
then A11: vn1 = vs . (n + 1) by PARTFUN1:def 8
.= vn1' by A10, PARTFUN1:def 8 ;
n in dom p' by A7, A8, FINSEQ_3:27;
then p' . n in rng p' by FUNCT_1:def 5;
then A12: ( 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 A3, Th40;
len p' <= len vs by A6, NAT_1:11;
then n <= len vs by A8, XXREAL_0:2;
then A13: n in dom vs by A7, FINSEQ_3:27;
then vn = vs . n by PARTFUN1:def 8
.= vn' by A13, PARTFUN1:def 8 ;
hence p' . n joins vs /. n,vs /. (n + 1) by A9, A12, A11, GRAPH_1:def 10; :: thesis: verum

end;

end;

then reconsider p'' = p' as Chain of G ;
p'' is one-to-one ;
hence p' is Path of ; :: thesis: verum