let G be _Graph; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum