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 :: thesis: ( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v )
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: 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;
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;
end;
end;
hence ( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v ) ; :: thesis: verum