let G1, G2 be _Graph; 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 ; ( G1 == G2 implies G1 .walkOf (x,e,y) = G2 .walkOf (x,e,y) )
assume A1:
G1 == G2
; G1 .walkOf (x,e,y) = G2 .walkOf (x,e,y)
now 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
;
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
;
verum end; suppose A4:
not
e Joins x,
y,
G1
;
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
;
verum end; end; end;
hence
G1 .walkOf (x,e,y) = G2 .walkOf (x,e,y)
; verum