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 A2, A1, FINSEQ_1:def 7; :: 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 A3, FINSEQ_1:1;

hence (W .addEdge e) . ((len W) + 2) = x by A2, A4, FINSEQ_1:def 7; :: 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 A2, FINSEQ_1:def 7; :: thesis: verum

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 A2, A1, FINSEQ_1:def 7; :: 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 A3, FINSEQ_1:1;

hence (W .addEdge e) . ((len W) + 2) = x by A2, A4, FINSEQ_1:def 7; :: 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 A2, FINSEQ_1:def 7; :: thesis: verum