let G be _Graph; :: thesis: for W being Walk of G
for e, v being set st e Joins W .last() ,v,G holds
(W .addEdge e) .length() = (W .length()) + 1
let W be Walk of G; :: thesis: for e, v being set st e Joins W .last() ,v,G holds
(W .addEdge e) .length() = (W .length()) + 1
let e, v be set ; :: thesis: ( e Joins W .last() ,v,G implies (W .addEdge e) .length() = (W .length()) + 1 )
assume e Joins W .last() ,v,G ; :: thesis: (W .addEdge e) .length() = (W .length()) + 1
then A1: (W .addEdge e) .edgeSeq() = (W .edgeSeq()) ^ <*e*> by GLIB_001:83;
len <*e*> = 1 by FINSEQ_1:56;
hence (W .addEdge e) .length() = (W .length()) + 1 by A1, FINSEQ_1:35; :: thesis: verum