let G be _Graph; 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; 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 ; ( 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
; (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;
hence
(W .addEdge e) .edgeSeq() = (W .edgeSeq()) ^ <*e*>
by A3, FINSEQ_1:14; verum