let G be _Graph; :: thesis: for W being vertex-distinct Walk of G
for e, v being object st e Joins W .last() ,v,G & not v in W .vertices() holds

let W be vertex-distinct Walk of G; :: thesis: for e, v being object st e Joins W .last() ,v,G & not v in W .vertices() holds

let e, v be object ; :: thesis: ( e Joins W .last() ,v,G & not v in W .vertices() implies W .addEdge e is vertex-distinct )
assume that
A1: e Joins W .last() ,v,G and
A2: not v in W .vertices() ; :: thesis:
set W2 = W .addEdge e;
A3: len (W .addEdge e) = (len W) + 2 by ;
A4: now :: thesis: for n being odd Element of NAT st n <= len (W .addEdge e) & n > len W holds
( n = len (W .addEdge e) & (W .addEdge e) . n = v )
let n be odd Element of NAT ; :: thesis: ( n <= len (W .addEdge e) & n > len W implies ( n = len (W .addEdge e) & (W .addEdge e) . n = v ) )
assume that
A5: n <= len (W .addEdge e) and
A6: n > len W ; :: thesis: ( n = len (W .addEdge e) & (W .addEdge e) . n = v )
(len W) + 1 <= n by ;
then (len W) + 1 < n by XXREAL_0:1;
then ((len W) + 1) + 1 <= n by NAT_1:13;
hence n = len (W .addEdge e) by ; :: thesis: (W .addEdge e) . n = v
hence (W .addEdge e) . n = v by A1, A3, Lm38; :: thesis: verum
end;
now :: thesis: for m, n being odd Element of NAT st m <= len (W .addEdge e) & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n holds
m = n
let m, n be odd Element of NAT ; :: thesis: ( m <= len (W .addEdge e) & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n implies m = n )
assume that
A7: m <= len (W .addEdge e) and
A8: n <= len (W .addEdge e) and
A9: (W .addEdge e) . m = (W .addEdge e) . n ; :: thesis: m = n
A10: 1 <= n by ABIAN:12;
A11: 1 <= m by ABIAN:12;
now :: thesis: m = n
per cases ( m <= len W or m > len W ) ;
suppose A12: m <= len W ; :: thesis: m = n
then m in dom W by ;
then A13: (W .addEdge e) . m = W . m by ;
now :: thesis: m = n
per cases ( n <= len W or n > len W ) ;
suppose A14: n <= len W ; :: thesis: m = n
then n in dom W by ;
then (W .addEdge e) . n = W . n by ;
hence m = n by A9, A12, A13, A14, Def29; :: thesis: verum
end;
suppose n > len W ; :: thesis: m = n
then W . m = v by A4, A8, A9, A13;
hence m = n by ; :: thesis: verum
end;
end;
end;
hence m = n ; :: thesis: verum
end;
suppose A15: m > len W ; :: thesis: m = n
then A16: (W .addEdge e) . m = v by A4, A7;
A17: m = len (W .addEdge e) by A4, A7, A15;
now :: thesis: m = n
per cases ( n <= len W or n > len W ) ;
suppose A18: n <= len W ; :: thesis: m = n
then n in dom W by ;
then v = W . n by A1, A9, A16, Lm38;
hence m = n by ; :: thesis: verum
end;
suppose n > len W ; :: thesis: m = n
hence m = n by A4, A8, A17; :: thesis: verum
end;
end;
end;
hence m = n ; :: thesis: verum
end;
end;
end;
hence m = n ; :: thesis: verum
end;
hence W .addEdge e is vertex-distinct ; :: thesis: verum