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 that
A1: W1A = W2A and
A2: W1B = W2B ; :: thesis: W1A .append W1B = W2A .append W2B
now :: thesis: W1A .append W1B = W2A .append W2B
per cases ( W1A .last() = W1B .first() or W1A .last() <> W1B .first() ) ;
suppose A3: W1A .last() = W1B .first() ; :: thesis: W1A .append W1B = W2A .append W2B
then A4: W2A .last() = W2B .first() by A1, A2;
thus W1A .append W1B = W1A ^' W1B by A3, Def10
.= W2A .append W2B by A1, A2, A4, Def10 ; :: thesis: verum
end;
suppose A5: W1A .last() <> W1B .first() ; :: thesis: W1A .append W1B = W2A .append W2B
then A6: W2A .last() <> W2B .first() by A1, A2;
thus W1A .append W1B = W2A by A1, A5, Def10
.= W2A .append W2B by A6, Def10 ; :: thesis: verum
end;
end;
end;
hence W1A .append W1B = W2A .append W2B ; :: thesis: verum