let G be WGraph; :: thesis: for W being Walk of G holds len (W .weightSeq()) = W .length()
let W be Walk of G; :: thesis: len (W .weightSeq()) = W .length()
thus len (W .weightSeq()) = len (W .edgeSeq()) by Def18
.= W .length() by GLIB_001:def 18 ; :: thesis: verum