let G1 be _Graph; :: thesis: for G2 being Subgraph of G1
for x, y, e being set st e Joins x,y,G2 holds
G1 .walkOf (x,e,y) = G2 .walkOf (x,e,y)
let G2 be Subgraph of G1; :: thesis: for x, y, e being set st e Joins x,y,G2 holds
G1 .walkOf (x,e,y) = G2 .walkOf (x,e,y)
let x, y, e be set ; :: thesis: ( e Joins x,y,G2 implies G1 .walkOf (x,e,y) = G2 .walkOf (x,e,y) )
assume A1: e Joins x,y,G2 ; :: thesis: G1 .walkOf (x,e,y) = G2 .walkOf (x,e,y)
then A2: e Joins x,y,G1 by GLIB_000:72;
G2 .walkOf (x,e,y) = <*x,e,y*> by A1, Def5;
hence G1 .walkOf (x,e,y) = G2 .walkOf (x,e,y) by A2, Def5; :: thesis: verum