scheme :: GLIB_009:sch 2
IndDWalk{ F1() -> _Graph, P1[ Walk of F1()] } :
for W being DWalk of F1() holds P1[W]
provided
A1: for W being V5() DWalk of F1() holds P1[W] and
A2: for W being DWalk of F1()
for e being object st e in (W .last()) .edgesOut() & P1[W] holds
P1[W .addEdge e]