let p be non empty Graph-yielding FinSequence; :: thesis: ( p . 1 is Path-like & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, e, v2 being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & ( p . n is _trivial or v1 in Endvertices (p . n) or v2 in Endvertices (p . n) ) ) ) implies p . (len p) is Path-like )
assume that
A1: p . 1 is Path-like and
A2: for n being Element of dom p st n <= (len p) - 1 holds
ex v1, e, v2 being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & ( p . n is _trivial or v1 in Endvertices (p . n) or v2 in Endvertices (p . n) ) ) ; :: thesis: p . (len p) is Path-like
defpred S₁[ Nat] means ( $1 <= (len p) - 1 implies p . ($1 + 1) is Path-like _Graph );
A3: S₁[ 0 ] by A1;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
assume A6: n + 1 <= (len p) - 1 ; :: thesis: p . ((n + 1) + 1) is Path-like _Graph
n + 0 <= n + 1 by XREAL_1:6;
then reconsider G2 = p . (n + 1) as Path-like _Graph by A5, A6, XXREAL_0:2;
(len p) - 1 <= (len p) - 0 by XREAL_1:10;
then A7: n + 1 <= len p by A6, XXREAL_0:2;
0 + 1 <= n + 1 by XREAL_1:6;
then reconsider n1 = n + 1 as Element of dom p by A7, FINSEQ_3:25;
consider v1, e, v2 being object such that
A8: p . (n1 + 1) is addAdjVertex of p . n1,v1,e,v2 and
A9: ( p . n1 is _trivial or v1 in Endvertices (p . n1) or v2 in Endvertices (p . n1) ) by A2, A6;

per cases ( v1 in Endvertices (p . n1) or v2 in Endvertices (p . n1) or p . n1 is _trivial ) by A9;

suppose A10: v1 in Endvertices (p . n1) ; :: thesis: p . ((n + 1) + 1) is Path-like _Graph

then reconsider v1 = v1 as Vertex of G2 ;
v1 is endvertex by A10, GLIB_006:56;
hence p . ((n + 1) + 1) is Path-like _Graph by A8, Th18; :: thesis: verum

end;

suppose A11: v2 in Endvertices (p . n1) ; :: thesis: p . ((n + 1) + 1) is Path-like _Graph

then reconsider v2 = v2 as Vertex of G2 ;
v2 is endvertex by A11, GLIB_006:56;
hence p . ((n + 1) + 1) is Path-like _Graph by A8, Th19; :: thesis: verum

end;

suppose A12: p . n1 is _trivial ; :: thesis: p . ((n + 1) + 1) is Path-like _Graph

per cases ( v1 in the_Vertices_of G2 or v2 in the_Vertices_of G2 or ( not v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 ) ) ;

suppose ( v1 in the_Vertices_of G2 or v2 in the_Vertices_of G2 ) ; :: thesis: p . ((n + 1) + 1) is Path-like _Graph

hence p . ((n + 1) + 1) is Path-like _Graph by A8, A12, Th18, Th19; :: thesis: verum

end;

suppose A13: ( not v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 ) ; :: thesis: p . ((n + 1) + 1) is Path-like _Graph

reconsider G1 = p . (n1 + 1) as addAdjVertex of p . n1,v1,e,v2 by A8;
G2 == G1 by A13, GLIB_006:def 12;
hence p . ((n + 1) + 1) is Path-like _Graph by Lm3; :: thesis: verum

end;

end;

end;

end;

end;

A14: for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
(len p) - 1 >= 1 - 1 by FINSEQ_1:20, XREAL_1:9;
then (len p) - 1 in NAT by INT_1:3;
then reconsider k = (len p) - 1 as Nat ;
S₁[k] by A14;
hence p . (len p) is Path-like ; :: thesis: verum