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

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