let G1, G2 be _Graph; :: thesis: for W1A, W1B being Walk of G1
for W2A, W2B being Walk of G2 st W1A = W2A & W1B = W2B holds
W1A .append W1B = W2A .append W2B
let W1A, W1B be Walk of G1; :: thesis: for W2A, W2B being Walk of G2 st W1A = W2A & W1B = W2B holds
W1A .append W1B = W2A .append W2B
let W2A, W2B be Walk of G2; :: thesis: ( W1A = W2A & W1B = W2B implies W1A .append W1B = W2A .append W2B )
assume A1: ( W1A = W2A & W1B = W2B ) ; :: thesis: W1A .append W1B = W2A .append W2B

now

per cases ( W1A .last() = W1B .first() or W1A .last() <> W1B .first() ) ;

suppose A2: W1A .last() = W1B .first() ; :: thesis: W1A .append W1B = W2A .append W2B

then A3: W2A .last() = W2B .first() by A1;
thus W1A .append W1B = W1A ^' W1B by A2, Def10
.= W2A .append W2B by A1, A3, Def10 ; :: thesis: verum

end;

suppose A4: W1A .last() <> W1B .first() ; :: thesis: W1A .append W1B = W2A .append W2B

then A5: W2A .last() <> W2B .first() by A1;
thus W1A .append W1B = W2A by A1, A4, Def10
.= W2A .append W2B by A5, Def10 ; :: thesis: verum

end;

end;

end;

hence W1A .append W1B = W2A .append W2B ; :: thesis: verum