let G be _Graph; :: thesis: for W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
(W .addEdge e) .vertexSeq() = (W .vertexSeq()) ^ <*x*>
let W be Walk of G; :: thesis: for e, x being set st e Joins W .last() ,x,G holds
(W .addEdge e) .vertexSeq() = (W .vertexSeq()) ^ <*x*>
let e, x be set ; :: thesis: ( e Joins W .last() ,x,G implies (W .addEdge e) .vertexSeq() = (W .vertexSeq()) ^ <*x*> )
set W2 = W .addEdge e;
set W3 = (W .vertexSeq()) ^ <*x*>;
assume A1: e Joins W .last() ,x,G ; :: thesis: (W .addEdge e) .vertexSeq() = (W .vertexSeq()) ^ <*x*>
then len (W .addEdge e) = (len W) + 2 by Lm37;
then A2: ((len W) + 2) + 1 = 2 * (len ((W .addEdge e) .vertexSeq())) by Def14;
len ((W .vertexSeq()) ^ <*x*>) = (len (W .vertexSeq())) + (len <*x*>) by FINSEQ_1:22;
then len ((W .vertexSeq()) ^ <*x*>) = (len (W .vertexSeq())) + 1 by FINSEQ_1:39;
then 2 * (len ((W .vertexSeq()) ^ <*x*>)) = (2 * (len (W .vertexSeq()))) + (2 * 1) ;
then A3: 2 * (len ((W .vertexSeq()) ^ <*x*>)) = ((len W) + 1) + 2 by Def14
.= 2 * (len ((W .addEdge e) .vertexSeq())) by A2 ;

now :: thesis: for k being Nat st 1 <= k & k <= len ((W .addEdge e) .vertexSeq()) holds
((W .addEdge e) .vertexSeq()) . k = ((W .vertexSeq()) ^ <*x*>) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len ((W .addEdge e) .vertexSeq()) implies ((W .addEdge e) .vertexSeq()) . k = ((W .vertexSeq()) ^ <*x*>) . k )
assume that
A4: 1 <= k and
A5: k <= len ((W .addEdge e) .vertexSeq()) ; :: thesis: ((W .addEdge e) .vertexSeq()) . k = ((W .vertexSeq()) ^ <*x*>) . k
A6: ((W .addEdge e) .vertexSeq()) . k = (W .addEdge e) . ((2 * k) - 1) by A4, A5, Def14;
A7: k in dom ((W .vertexSeq()) ^ <*x*>) by A3, A4, A5, FINSEQ_3:25;

now :: thesis: ((W .addEdge e) .vertexSeq()) . k = ((W .vertexSeq()) ^ <*x*>) . k

per cases ( k in dom (W .vertexSeq()) or ex n being Nat st
( n in dom <*x*> & k = (len (W .vertexSeq())) + n ) ) by A7, FINSEQ_1:25;

suppose A8: k in dom (W .vertexSeq()) ; :: thesis: ((W .addEdge e) .vertexSeq()) . k = ((W .vertexSeq()) ^ <*x*>) . k

then A9: (2 * k) - 1 in dom W by Th71;
A10: 1 <= k by A8, FINSEQ_3:25;
A11: k <= len (W .vertexSeq()) by A8, FINSEQ_3:25;
((W .vertexSeq()) ^ <*x*>) . k = (W .vertexSeq()) . k by A8, FINSEQ_1:def 7;
then ((W .vertexSeq()) ^ <*x*>) . k = W . ((2 * k) - 1) by A10, A11, Def14;
hence ((W .addEdge e) .vertexSeq()) . k = ((W .vertexSeq()) ^ <*x*>) . k by A1, A6, A9, Lm38; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom <*x*> & k = (len (W .vertexSeq())) + n ) ; :: thesis: ((W .addEdge e) .vertexSeq()) . k = ((W .vertexSeq()) ^ <*x*>) . k

then consider n being Nat such that
A12: n in dom <*x*> and
A13: k = (len (W .vertexSeq())) + n ;
n in Seg 1 by A12, FINSEQ_1:38;
then A14: n = 1 by FINSEQ_1:2, TARSKI:def 1;
then A15: 2 * k = (2 * (len (W .vertexSeq()))) + (2 * 1) by A13
.= ((len W) + 1) + 2 by Def14
.= ((len W) + 2) + 1 ;
((W .vertexSeq()) ^ <*x*>) . k = <*x*> . 1 by A12, A13, A14, FINSEQ_1:def 7
.= x ;
hence ((W .addEdge e) .vertexSeq()) . k = ((W .vertexSeq()) ^ <*x*>) . k by A1, A6, A15, Lm38; :: thesis: verum

end;

end;

end;

hence ((W .addEdge e) .vertexSeq()) . k = ((W .vertexSeq()) ^ <*x*>) . k ; :: thesis: verum

end;

hence (W .addEdge e) .vertexSeq() = (W .vertexSeq()) ^ <*x*> by A3, FINSEQ_1:14; :: thesis: verum