let G be _Graph; :: thesis: for v being Vertex of G holds (G .walkOf v) .edges() = {}
let v be Vertex of G; :: thesis: (G .walkOf v) .edges() = {}
A1: (G .walkOf v) .edgeSeq() = <*> (the_Edges_of G) by Th24
.= {} ;
thus (G .walkOf v) .edges() = rng {} by A1, GLIB_001:def 17
.= {} ; :: thesis: verum