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) .length() = (W .length()) + 1
let W be Walk of G; :: thesis: for e, x being object st e Joins W .last() ,x,G holds
(W .addEdge e) .length() = (W .length()) + 1
let e, x be object ; :: thesis: ( e Joins W .last() ,x,G implies (W .addEdge e) .length() = (W .length()) + 1 )
assume A1: e Joins W .last() ,x,G ; :: thesis: (W .addEdge e) .length() = (W .length()) + 1
(2 * ((W .addEdge e) .length())) + 1 = len (W .addEdge e) by GLIB_001:112
.= (len W) + 2 by A1, GLIB_001:64
.= ((2 * (W .length())) + 1) + 2 by GLIB_001:112
.= (2 * ((W .length()) + 1)) + 1 ;
hence (W .addEdge e) .length() = (W .length()) + 1 ; :: thesis: verum