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

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 W2Bend;

hence
W1A .append W1B = W2A .append W2B
; :: thesis: verumper cases
( W1A .last() = W1B .first() or W1A .last() <> W1B .first() )
;

end;