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

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