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 )

now

per cases ( v in W1 .vertices() or not v in W1 .vertices() ) ;

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

then A3: v in W2 .vertices() by A1, Th77;
( W1 .find v <= len W2 & W2 . (W1 .find v) = v & ( for n being odd Nat st n <= len W2 & W2 . n = v holds
W1 .find v <= n ) ) by A1, A2, Def19;
hence W1 .find v = W2 .find v by A3, Def19; :: thesis: W1 .rfind v = W2 .rfind v
( W1 .rfind v <= len W2 & W2 . (W1 .rfind v) = v & ( for n being odd Element of NAT st n <= len W2 & W2 . n = v holds
n <= W1 .rfind v ) ) by A1, A2, Def21;
hence W1 .rfind v = W2 .rfind v by A3, Def21; :: thesis: verum

end;

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

then A5: not v in W2 .vertices() by A1, Th77;
thus W1 .find v = len W2 by A1, A4, Def19
.= W2 .find v by A5, Def19 ; :: thesis: W1 .rfind v = W2 .rfind v
thus W1 .rfind v = len W2 by A1, A4, Def21
.= W2 .rfind v by A5, Def21 ; :: thesis: verum

end;

end;

end;

hence ( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v ) ; :: thesis: verum