let G be _Graph; :: thesis: for W being Walk of G
for e, v being object st W is Path-like & e Joins W .last() ,v,G & not e in W .edges() & ( W is trivial or W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds
W . n <> v ) holds
W .addEdge e is Path-like

let W be Walk of G; :: thesis: for e, v being object st W is Path-like & e Joins W .last() ,v,G & not e in W .edges() & ( W is trivial or W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds
W . n <> v ) holds
W .addEdge e is Path-like

let e, v be object ; :: thesis: ( W is Path-like & e Joins W .last() ,v,G & not e in W .edges() & ( W is trivial or W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds
W . n <> v ) implies W .addEdge e is Path-like )

assume that
A1: W is Path-like and
A2: e Joins W .last() ,v,G and
A3: not e in W .edges() and
A4: ( W is trivial or W is open ) and
A5: for n being odd Element of NAT st 1 < n & n <= len W holds
W . n <> v ; :: thesis:
reconsider lenW = len W as odd Element of NAT ;
set W2 = W .addEdge e;
A6: e in () .edgesInOut() by ;
now :: thesis: ( W .addEdge e is Trail-like & ( for m, n being odd Element of NAT st m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n holds
( m = 1 & n = len (W .addEdge e) ) ) )
W is Trail-like by A1;
hence W .addEdge e is Trail-like by A3, A6, Lm60; :: thesis: for m, n being odd Element of NAT st m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n holds
( m = 1 & n = len (W .addEdge e) )

let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n implies ( m = 1 & n = len (W .addEdge e) ) )
assume that
A7: m < n and
A8: n <= len (W .addEdge e) and
A9: (W .addEdge e) . m = (W .addEdge e) . n ; :: thesis: ( m = 1 & n = len (W .addEdge e) )
now :: thesis: ( m = 1 & n = len (W .addEdge e) )
per cases ( W is open or W is trivial ) by A4;
suppose A10: W is open ; :: thesis: ( m = 1 & n = len (W .addEdge e) )
now :: thesis: ( m = 1 & n = len (W .addEdge e) )
per cases ( n <= len W or n > len W ) ;
suppose A11: n <= len W ; :: thesis: ( m = 1 & n = len (W .addEdge e) )
A12: 1 <= m by ABIAN:12;
m <= len W by ;
then m in dom W by ;
then A13: (W .addEdge e) . m = W . m by ;
1 <= n by ABIAN:12;
then n in dom W by ;
then A14: W . m = W . n by A2, A9, A13, Lm38;
then m = 1 by A1, A7, A11;
then W .first() = W .last() by A1, A7, A11, A14;
hence ( m = 1 & n = len (W .addEdge e) ) by A10; :: thesis: verum
end;
suppose n > len W ; :: thesis: ( m = 1 & n = len (W .addEdge e) )
then lenW + 1 <= n by NAT_1:13;
then lenW + 1 < n by XXREAL_0:1;
then (lenW + 1) + 1 <= n by NAT_1:13;
then (len W) + (1 + 1) <= n ;
then A15: len (W .addEdge e) <= n by ;
then n = len (W .addEdge e) by ;
then (W .addEdge e) . n = (W .addEdge e) . ((len W) + 2) by ;
then A16: (W .addEdge e) . n = v by ;
m < len (W .addEdge e) by ;
then m < (len W) + (1 + 1) by ;
then m < ((len W) + 1) + 1 ;
then m <= lenW + 1 by NAT_1:13;
then m < lenW + 1 by XXREAL_0:1;
then A17: m <= len W by NAT_1:13;
1 <= m by ABIAN:12;
then m in dom W by ;
then A18: W . m = v by A2, A9, A16, Lm38;
now :: thesis: not m <> 1
A19: 1 <= m by ABIAN:12;
assume m <> 1 ; :: thesis: contradiction
then 1 < m by ;
hence contradiction by A5, A17, A18; :: thesis: verum
end;
hence m = 1 ; :: thesis: n = len (W .addEdge e)
thus n = len (W .addEdge e) by ; :: thesis: verum
end;
end;
end;
hence ( m = 1 & n = len (W .addEdge e) ) ; :: thesis: verum
end;
suppose W is trivial ; :: thesis: ( m = 1 & n = len (W .addEdge e) )
then ex v being Vertex of G st W = G .walkOf v by Lm56;
then len W = 1 by FINSEQ_1:39;
then A20: len (W .addEdge e) = 1 + 2 by ;
A21: m + 1 <= n by ;
A22: 1 <= m by ABIAN:12;
then 1 + 1 <= m + 1 by XREAL_1:7;
then 2 * 1 <= n by ;
then 2 * 1 < n by XXREAL_0:1;
then A23: len (W .addEdge e) <= n by ;
then n = len (W .addEdge e) by ;
then (m + 1) - 1 <= 3 - 1 by ;
then m < 2 * 1 by XXREAL_0:1;
then m + 1 <= 2 by NAT_1:13;
then (m + 1) - 1 <= 2 - 1 by XREAL_1:13;
hence ( m = 1 & n = len (W .addEdge e) ) by ; :: thesis: verum
end;
end;
end;
hence ( m = 1 & n = len (W .addEdge e) ) ; :: thesis: verum
end;
hence W .addEdge e is Path-like ; :: thesis: verum