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: G2 .walkOf x,e,y = <*x,e,y*> by Def5;
e Joins x,y,G1 by A1, GLIB_000:75;
hence G1 .walkOf x,e,y = G2 .walkOf x,e,y by A2, Def5; :: thesis: verum