let G1, G2 be _Graph; :: thesis: for e, x, y being set st G1 == G2 holds
G1 .walkOf (x,e,y) = G2 .walkOf (x,e,y)
let e, x, 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 :: thesis: G1 .walkOf (x,e,y) = G2 .walkOf (x,e,y)
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:88;
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:88;
A6: the_Vertices_of G1 = the_Vertices_of G2 by A1, GLIB_000:def 34;
thus G1 .walkOf (x,e,y) = G1 .walkOf the Element of the_Vertices_of G1 by A4, Def5
.= G2 .walkOf the Element of the_Vertices_of G2 by A6
.= 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