let G1, G2 be _Graph; :: thesis: for x, e, y being set st G1 == G2 holds
G1 .walkOf x,e,y = G2 .walkOf x,e,y
let x, e, y be set ; :: thesis: ( G1 == G2 implies G1 .walkOf x,e,y = G2 .walkOf x,e,y )
assume A1: G1 == G2 ; :: thesis: G1 .walkOf x,e,y = G2 .walkOf x,e,y

now

per cases ( e Joins x,y,G1 or not e Joins x,y,G1 ) ;

suppose A2: e Joins x,y,G1 ; :: thesis: G1 .walkOf x,e,y = G2 .walkOf x,e,y

then A3: e Joins x,y,G2 by A1, GLIB_000:91;
thus G1 .walkOf x,e,y = <*x,e,y*> by A2, Def5
.= G2 .walkOf x,e,y by A3, Def5 ; :: thesis: verum

end;

suppose A4: not e Joins x,y,G1 ; :: thesis: G1 .walkOf x,e,y = G2 .walkOf x,e,y

then A5: not e Joins x,y,G2 by A1, GLIB_000:91;
thus G1 .walkOf x,e,y = G1 .walkOf (choose (the_Vertices_of G1)) by A4, Def5
.= G2 .walkOf (choose (the_Vertices_of G2)) by A1, GLIB_000:def 36
.= G2 .walkOf x,e,y by A5, Def5 ; :: thesis: verum

end;

end;

end;

hence G1 .walkOf x,e,y = G2 .walkOf x,e,y ; :: thesis: verum