let p be non empty Graph-yielding FinSequence; :: thesis: ( not p . 1 is _trivial & 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 & ( v1 in Endvertices (p . n) or v2 in Endvertices (p . n) ) ) ) implies p . (len p) is Path-like )
assume that
A1: ( not p . 1 is _trivial & 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 & ( 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: ( 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) ) 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;

end;

end;

A12: 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 A12;
hence p . (len p) is Path-like ; :: thesis: verum