let G be _Graph; :: thesis: for W1, W2 being Walk of G holds W1 is_a_prefix_of W1 .append W2
let W1, W2 be Walk of G; :: thesis: W1 is_a_prefix_of W1 .append W2
set W1a = W1 .append W2;
per cases ( W1 .last() = W2 .first() or W1 .last() <> W2 .first() ) ;
suppose W1 .last() = W2 .first() ; :: thesis: W1 is_a_prefix_of W1 .append W2
then len W1 <= len (W1 .append W2) by GLIB_001:29;
then A1: dom W1 c= dom (W1 .append W2) by FINSEQ_3:30;
for x being object st x in dom W1 holds
W1 . x = (W1 .append W2) . x by GLIB_001:32;
hence W1 is_a_prefix_of W1 .append W2 by A1, GRFUNC_1:2; :: thesis: verum
end;
suppose W1 .last() <> W2 .first() ; :: thesis: W1 is_a_prefix_of W1 .append W2
hence W1 is_a_prefix_of W1 .append W2 by GLIB_001:def 10; :: thesis: verum
end;
end;