let G be _Graph; :: thesis: for v being Vertex of G holds (G .walkOf v) .edgeSeq() = <*> (the_Edges_of G)
let v be Vertex of G; :: thesis: (G .walkOf v) .edgeSeq() = <*> (the_Edges_of G)
set W = G .walkOf v;
len (G .walkOf v) = (2 * (len ((G .walkOf v) .edgeSeq()))) + 1 by GLIB_001:def 15;
then 1 - 1 = ((2 * (len ((G .walkOf v) .edgeSeq()))) + 1) - 1 by GLIB_001:13;
hence (G .walkOf v) .edgeSeq() = <*> (the_Edges_of G) ; :: thesis: verum