let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds
len W1 = len W2
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds
len W1 = len W2
let W2 be Walk of G2; :: thesis: ( W1 .vertexSeq() = W2 .vertexSeq() implies len W1 = len W2 )
assume A1: W1 .vertexSeq() = W2 .vertexSeq() ; :: thesis: len W1 = len W2
(len W1) + 1 = 2 * (len (W1 .vertexSeq())) by GLIB_001:def 14
.= (len W2) + 1 by A1, GLIB_001:def 14 ;
hence len W1 = len W2 ; :: thesis: verum