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() = (W .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() = (W .edgeSeq()) ^ <*e*>
let e, x be object ; :: thesis: ( e Joins W .last() ,x,G implies (W .addEdge e) .edgeSeq() = (W .edgeSeq()) ^ <*e*> )
set W2 = W .addEdge e;
set W3 = (W .edgeSeq()) ^ <*e*>;
assume A1: e Joins W .last() ,x,G ; :: thesis: (W .addEdge e) .edgeSeq() = (W .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 (W .edgeSeq()))) + 1) = (2 * (len ((W .addEdge e) .edgeSeq()))) + 1 by Def15;
then A2: 2 * ((len (W .edgeSeq())) + 1) = 2 * (len ((W .addEdge e) .edgeSeq())) ;
len ((W .edgeSeq()) ^ <*e*>) = (len (W .edgeSeq())) + (len <*e*>) by FINSEQ_1:22;
then A3: 2 * (len ((W .edgeSeq()) ^ <*e*>)) = 2 * (len ((W .addEdge e) .edgeSeq())) by A2, FINSEQ_1:39;

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

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

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

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

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

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

end;

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

then consider n being Element of NAT such that
A12: n in dom <*e*> and
A13: k = (len (W .edgeSeq())) + n ;
n in {1} by A12, FINSEQ_1:2, FINSEQ_1:38;
then A14: n = 1 by TARSKI:def 1;
then A15: 2 * k = ((2 * (len (W .edgeSeq()))) + 1) + 1 by A13
.= (len W) + 1 by Def15 ;
((W .edgeSeq()) ^ <*e*>) . k = <*e*> . 1 by A12, A13, A14, FINSEQ_1:def 7
.= e ;
hence ((W .addEdge e) .edgeSeq()) . k = ((W .edgeSeq()) ^ <*e*>) . k by A1, A6, A15, Lm38; :: thesis: verum

end;

end;

end;

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

end;

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