let G be _Graph; :: thesis: for W being vertex-distinct Walk of G
for e, v being set st e Joins W .last() ,v,G & not v in W .vertices() holds
W .addEdge e is vertex-distinct
let W be vertex-distinct Walk of G; :: thesis: for e, v being set st e Joins W .last() ,v,G & not v in W .vertices() holds
W .addEdge e is vertex-distinct
let e, v be set ; :: thesis: ( e Joins W .last() ,v,G & not v in W .vertices() implies W .addEdge e is vertex-distinct )
assume A1: ( e Joins W .last() ,v,G & not v in W .vertices() ) ; :: thesis: W .addEdge e is vertex-distinct
set W2 = W .addEdge e;
A2: len (W .addEdge e) = (len W) + 2 by A1, Lm37;

A3: now

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 A4: ( n <= len (W .addEdge e) & n > len W ) ; :: thesis: ( n = len (W .addEdge e) & (W .addEdge e) . n = v )
then (len W) + 1 <= n by NAT_1:13;
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 A2, A4, XXREAL_0:1; :: thesis: (W .addEdge e) . n = v
hence (W .addEdge e) . n = v by A1, A2, Lm38; :: thesis: verum

end;

now

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 A5: ( m <= len (W .addEdge e) & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n ) ; :: thesis: m = n
A6: ( 1 <= m & 1 <= n ) by HEYTING3:1;

now

per cases ( m <= len W or m > len W ) ;

suppose A7: m <= len W ; :: thesis: m = n

then m in dom W by A6, FINSEQ_3:27;
then A8: (W .addEdge e) . m = W . m by A1, Lm38;

now

per cases ( n <= len W or n > len W ) ;

suppose A9: n <= len W ; :: thesis: m = n

then n in dom W by A6, FINSEQ_3:27;
then (W .addEdge e) . n = W . n by A1, Lm38;
hence m = n by A5, A7, A8, A9, Def29; :: thesis: verum

end;

suppose n > len W ; :: thesis: m = n

then ( n = len (W .addEdge e) & W . m = v ) by A3, A5, A8;
hence m = n by A1, A7, Lm45; :: thesis: verum

end;

end;

end;

hence m = n ; :: thesis: verum

end;

suppose m > len W ; :: thesis: m = n

then A10: ( m = len (W .addEdge e) & (W .addEdge e) . m = v ) by A3, A5;

now

per cases ( n <= len W or n > len W ) ;

suppose A11: n <= len W ; :: thesis: m = n

then n in dom W by A6, FINSEQ_3:27;
then v = W . n by A1, A5, A10, Lm38;
hence m = n by A1, A11, Lm45; :: thesis: verum

end;

suppose n > len W ; :: thesis: m = n

hence m = n by A3, A5, A10; :: 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 by Def29; :: thesis: verum