let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1

for W2 being Walk of G2

for v being set st W1 = W2 holds

( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v )

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2

for v being set st W1 = W2 holds

( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v )

let W2 be Walk of G2; :: thesis: for v being set st W1 = W2 holds

( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v )

let v be set ; :: thesis: ( W1 = W2 implies ( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v ) )

assume A1: W1 = W2 ; :: thesis: ( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v )

for W2 being Walk of G2

for v being set st W1 = W2 holds

( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v )

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2

for v being set st W1 = W2 holds

( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v )

let W2 be Walk of G2; :: thesis: for v being set st W1 = W2 holds

( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v )

let v be set ; :: thesis: ( W1 = W2 implies ( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v ) )

assume A1: W1 = W2 ; :: thesis: ( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v )

now :: thesis: ( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v )end;

hence
( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v )
; :: thesis: verumper cases
( v in W1 .vertices() or not v in W1 .vertices() )
;

end;

suppose A2:
v in W1 .vertices()
; :: thesis: ( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v )

then A3:
W2 . (W1 .find v) = v
by A1, Def19;

A4: v in W2 .vertices() by A1, A2, Th74;

A5: for n being odd Nat st n <= len W2 & W2 . n = v holds

W1 .find v <= n by A1, A2, Def19;

W1 .find v <= len W2 by A1, A2, Def19;

hence W1 .find v = W2 .find v by A4, A3, A5, Def19; :: thesis: W1 .rfind v = W2 .rfind v

A6: W2 . (W1 .rfind v) = v by A1, A2, Def21;

A7: for n being odd Element of NAT st n <= len W2 & W2 . n = v holds

n <= W1 .rfind v by A1, A2, Def21;

W1 .rfind v <= len W2 by A1, A2, Def21;

hence W1 .rfind v = W2 .rfind v by A4, A6, A7, Def21; :: thesis: verum

end;A4: v in W2 .vertices() by A1, A2, Th74;

A5: for n being odd Nat st n <= len W2 & W2 . n = v holds

W1 .find v <= n by A1, A2, Def19;

W1 .find v <= len W2 by A1, A2, Def19;

hence W1 .find v = W2 .find v by A4, A3, A5, Def19; :: thesis: W1 .rfind v = W2 .rfind v

A6: W2 . (W1 .rfind v) = v by A1, A2, Def21;

A7: for n being odd Element of NAT st n <= len W2 & W2 . n = v holds

n <= W1 .rfind v by A1, A2, Def21;

W1 .rfind v <= len W2 by A1, A2, Def21;

hence W1 .rfind v = W2 .rfind v by A4, A6, A7, Def21; :: thesis: verum

suppose A8:
not v in W1 .vertices()
; :: thesis: ( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v )

then A9:
not v in W2 .vertices()
by A1, Th74;

thus W1 .find v = len W2 by A1, A8, Def19

.= W2 .find v by A9, Def19 ; :: thesis: W1 .rfind v = W2 .rfind v

thus W1 .rfind v = len W2 by A1, A8, Def21

.= W2 .rfind v by A9, Def21 ; :: thesis: verum

end;thus W1 .find v = len W2 by A1, A8, Def19

.= W2 .find v by A9, Def19 ; :: thesis: W1 .rfind v = W2 .rfind v

thus W1 .rfind v = len W2 by A1, A8, Def21

.= W2 .rfind v by A9, Def21 ; :: thesis: verum