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() = () ^ <*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() = () ^ <*x*>

let e, x be set ; :: thesis: ( e Joins W .last() ,x,G implies (W .addEdge e) .vertexSeq() = () ^ <*x*> )
set W2 = W .addEdge e;
set W3 = () ^ <*x*>;
assume A1: e Joins W .last() ,x,G ; :: thesis: (W .addEdge e) .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 (() ^ <*x*>) = (len ()) + () by FINSEQ_1:22;
then len (() ^ <*x*>) = (len ()) + 1 by FINSEQ_1:39;
then 2 * (len (() ^ <*x*>)) = (2 * (len ())) + (2 * 1) ;
then A3: 2 * (len (() ^ <*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 = (() ^ <*x*>) . k
let k be Nat; :: thesis: ( 1 <= k & k <= len ((W .addEdge e) .vertexSeq()) implies ((W .addEdge e) .vertexSeq()) . k = (() ^ <*x*>) . k )
assume that
A4: 1 <= k and
A5: k <= len ((W .addEdge e) .vertexSeq()) ; :: thesis: ((W .addEdge e) .vertexSeq()) . k = (() ^ <*x*>) . k
A6: ((W .addEdge e) .vertexSeq()) . k = (W .addEdge e) . ((2 * k) - 1) by ;
A7: k in dom (() ^ <*x*>) by ;
now :: thesis: ((W .addEdge e) .vertexSeq()) . k = (() ^ <*x*>) . k
per cases ( k in dom () or ex n being Nat st
( n in dom <*x*> & k = (len ()) + n ) )
by ;
suppose A8: k in dom () ; :: thesis: ((W .addEdge e) .vertexSeq()) . k = (() ^ <*x*>) . k
then A9: (2 * k) - 1 in dom W by Th71;
A10: 1 <= k by ;
A11: k <= len () by ;
((W .vertexSeq()) ^ <*x*>) . k = () . k by ;
then ((W .vertexSeq()) ^ <*x*>) . k = W . ((2 * k) - 1) by ;
hence ((W .addEdge e) .vertexSeq()) . k = (() ^ <*x*>) . k by A1, A6, A9, Lm38; :: thesis: verum
end;
suppose ex n being Nat st
( n in dom <*x*> & k = (len ()) + n ) ; :: thesis: ((W .addEdge e) .vertexSeq()) . k = (() ^ <*x*>) . k
then consider n being Nat such that
A12: n in dom <*x*> and
A13: k = (len ()) + n ;
n in Seg 1 by ;
then A14: n = 1 by ;
then A15: 2 * k = (2 * (len ())) + (2 * 1) by A13
.= ((len W) + 1) + 2 by Def14
.= ((len W) + 2) + 1 ;
(() ^ <*x*>) . k = <*x*> . 1 by
.= x by FINSEQ_1:def 8 ;
hence ((W .addEdge e) .vertexSeq()) . k = (() ^ <*x*>) . k by A1, A6, A15, Lm38; :: thesis: verum
end;
end;
end;
hence ((W .addEdge e) .vertexSeq()) . k = (() ^ <*x*>) . k ; :: thesis: verum
end;
hence (W .addEdge e) .vertexSeq() = () ^ <*x*> by ; :: thesis: verum