let G be _Graph; for W1, W2, W3 being Walk of G
for u, v being object holds
( W1 is_Walk_from u,v iff W1 .replaceWith (W2,W3) is_Walk_from u,v )
let W1, W2, W3 be Walk of G; for u, v being object holds
( W1 is_Walk_from u,v iff W1 .replaceWith (W2,W3) is_Walk_from u,v )
let u, v be object ; ( W1 is_Walk_from u,v iff W1 .replaceWith (W2,W3) is_Walk_from u,v )
( W1 is_Walk_from u,v iff ( W1 .first() = u & W1 .last() = v ) )
by GLIB_001:def 23;
then
( W1 is_Walk_from u,v iff ( u = (W1 .replaceWith (W2,W3)) .first() & v = (W1 .replaceWith (W2,W3)) .last() ) )
by Th39;
hence
( W1 is_Walk_from u,v iff W1 .replaceWith (W2,W3) is_Walk_from u,v )
by GLIB_001:def 23; verum