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 ;
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 ;
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