let G be _Graph; :: thesis: for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
( (W .addEdge e) . ((len W) + 1) = e & (W .addEdge e) . ((len W) + 2) = x & ( for n being Element of NAT st n in dom W holds
(W .addEdge e) . n = W . n ) )

let W be Walk of G; :: thesis: for e, x being object st e Joins W .last() ,x,G holds
( (W .addEdge e) . ((len W) + 1) = e & (W .addEdge e) . ((len W) + 2) = x & ( for n being Element of NAT st n in dom W holds
(W .addEdge e) . n = W . n ) )

let e, x be object ; :: thesis: ( e Joins W .last() ,x,G implies ( (W .addEdge e) . ((len W) + 1) = e & (W .addEdge e) . ((len W) + 2) = x & ( for n being Element of NAT st n in dom W holds
(W .addEdge e) . n = W . n ) ) )

set W2 = W .addEdge e;
A1: <*e,x*> . 1 = e by FINSEQ_1:44;
assume e Joins W .last() ,x,G ; :: thesis: ( (W .addEdge e) . ((len W) + 1) = e & (W .addEdge e) . ((len W) + 2) = x & ( for n being Element of NAT st n in dom W holds
(W .addEdge e) . n = W . n ) )

then A2: W .addEdge e = W ^ <*e,x*> by Lm35;
A3: dom <*e,x*> = Seg 2 by FINSEQ_1:89;
then 1 in dom <*e,x*> by FINSEQ_1:1;
hence (W .addEdge e) . ((len W) + 1) = e by ; :: thesis: ( (W .addEdge e) . ((len W) + 2) = x & ( for n being Element of NAT st n in dom W holds
(W .addEdge e) . n = W . n ) )

A4: <*e,x*> . 2 = x by FINSEQ_1:44;
2 in dom <*e,x*> by ;
hence (W .addEdge e) . ((len W) + 2) = x by ; :: thesis: for n being Element of NAT st n in dom W holds
(W .addEdge e) . n = W . n

let n be Element of NAT ; :: thesis: ( n in dom W implies (W .addEdge e) . n = W . n )
assume n in dom W ; :: thesis: (W .addEdge e) . n = W . n
hence (W .addEdge e) . n = W . n by ; :: thesis: verum