let G be _Graph; :: thesis: for W1, W2 being Walk of G
for x, y, z being set st W1 is_Walk_from x,y & W2 is_Walk_from y,z holds
W1 .append W2 is_Walk_from x,z
let W1, W2 be Walk of G; :: thesis: for x, y, z being set st W1 is_Walk_from x,y & W2 is_Walk_from y,z holds
W1 .append W2 is_Walk_from x,z
let x, y, z be set ; :: thesis: ( W1 is_Walk_from x,y & W2 is_Walk_from y,z implies W1 .append W2 is_Walk_from x,z )
assume that
A1: W1 is_Walk_from x,y and
A2: W2 is_Walk_from y,z ; :: thesis: W1 .append W2 is_Walk_from x,z
A3: W1 .last() = y by A1, Def23;
A4: W2 .last() = z by A2, Def23;
A5: W2 .first() = y by A2, Def23;
W1 .first() = x by A1, Def23;
hence W1 .append W2 is_Walk_from x,z by A3, A5, A4, Lm11; :: thesis: verum