let G be _Graph; :: thesis: for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
for n being Nat st n in dom W holds
( (W .addEdge e) . n = W . n & n in dom (W .addEdge e) )
let W be Walk of G; :: thesis: for e, x being object st e Joins W .last() ,x,G holds
for n being Nat st n in dom W holds
( (W .addEdge e) . n = W . n & n in dom (W .addEdge e) )
let e, x be object ; :: thesis: ( e Joins W .last() ,x,G implies for n being Nat st n in dom W holds
( (W .addEdge e) . n = W . n & n in dom (W .addEdge e) ) )
assume A1: e Joins W .last() ,x,G ; :: thesis: for n being Nat st n in dom W holds
( (W .addEdge e) . n = W . n & n in dom (W .addEdge e) )
let n be Nat; :: thesis: ( n in dom W implies ( (W .addEdge e) . n = W . n & n in dom (W .addEdge e) ) )
assume A2: n in dom W ; :: thesis: ( (W .addEdge e) . n = W . n & n in dom (W .addEdge e) )
thus (W .addEdge e) . n = W . n by A1, A2, GLIB_001:65; :: thesis: n in dom (W .addEdge e)
A3: 1 <= n by A2, FINSEQ_3:25;
A4: len W < (len W) + 2 by XREAL_1:29;
n <= len W by A2, FINSEQ_3:25;
then A5: n <= (len W) + 2 by A4, XXREAL_0:2;
len (W .addEdge e) = (len W) + 2 by A1, GLIB_001:64;
hence n in dom (W .addEdge e) by A3, A5, FINSEQ_3:25; :: thesis: verum