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) .edgeSeq() = () ^ <*e*>

let W be Walk of G; :: thesis: for e, x being object st e Joins W .last() ,x,G holds
(W .addEdge e) .edgeSeq() = () ^ <*e*>

let e, x be object ; :: thesis: ( e Joins W .last() ,x,G implies (W .addEdge e) .edgeSeq() = () ^ <*e*> )
set W2 = W .addEdge e;
set W3 = () ^ <*e*>;
assume A1: e Joins W .last() ,x,G ; :: thesis: (W .addEdge e) .edgeSeq() = () ^ <*e*>
then len (W .addEdge e) = (len W) + 2 by Lm37;
then (len W) + 2 = (2 * (len ((W .addEdge e) .edgeSeq()))) + 1 by Def15;
then 2 + ((2 * (len ())) + 1) = (2 * (len ((W .addEdge e) .edgeSeq()))) + 1 by Def15;
then A2: 2 * ((len ()) + 1) = 2 * (len ((W .addEdge e) .edgeSeq())) ;
len (() ^ <*e*>) = (len ()) + () by FINSEQ_1:22;
then A3: 2 * (len (() ^ <*e*>)) = 2 * (len ((W .addEdge e) .edgeSeq())) by ;
now :: thesis: for k being Nat st 1 <= k & k <= len ((W .addEdge e) .edgeSeq()) holds
((W .addEdge e) .edgeSeq()) . k = (() ^ <*e*>) . k
let k be Nat; :: thesis: ( 1 <= k & k <= len ((W .addEdge e) .edgeSeq()) implies ((W .addEdge e) .edgeSeq()) . k = (() ^ <*e*>) . k )
assume that
A4: 1 <= k and
A5: k <= len ((W .addEdge e) .edgeSeq()) ; :: thesis: ((W .addEdge e) .edgeSeq()) . k = (() ^ <*e*>) . k
A6: ((W .addEdge e) .edgeSeq()) . k = (W .addEdge e) . (2 * k) by ;
A7: k in dom (() ^ <*e*>) by ;
now :: thesis: ((W .addEdge e) .edgeSeq()) . k = (() ^ <*e*>) . k
per cases ( k in dom () or ex n being Nat st
( n in dom <*e*> & k = (len ()) + n ) )
by ;
suppose A8: k in dom () ; :: thesis: ((W .addEdge e) .edgeSeq()) . k = (() ^ <*e*>) . k
then A9: 2 * k in dom W by Lm41;
A10: 1 <= k by ;
A11: k <= len () by ;
((W .edgeSeq()) ^ <*e*>) . k = () . k by ;
then ((W .edgeSeq()) ^ <*e*>) . k = W . (2 * k) by ;
hence ((W .addEdge e) .edgeSeq()) . k = (() ^ <*e*>) . k by A1, A6, A9, Lm38; :: thesis: verum
end;
suppose ex n being Nat st
( n in dom <*e*> & k = (len ()) + n ) ; :: thesis: ((W .addEdge e) .edgeSeq()) . k = (() ^ <*e*>) . k
then consider n being Element of NAT such that
A12: n in dom <*e*> and
A13: k = (len ()) + n ;
n in {1} by ;
then A14: n = 1 by TARSKI:def 1;
then A15: 2 * k = ((2 * (len ())) + 1) + 1 by A13
.= (len W) + 1 by Def15 ;
(() ^ <*e*>) . k = <*e*> . 1 by
.= e by FINSEQ_1:def 8 ;
hence ((W .addEdge e) .edgeSeq()) . k = (() ^ <*e*>) . k by A1, A6, A15, Lm38; :: thesis: verum
end;
end;
end;
hence ((W .addEdge e) .edgeSeq()) . k = (() ^ <*e*>) . k ; :: thesis: verum
end;
hence (W .addEdge e) .edgeSeq() = () ^ <*e*> by ; :: thesis: verum