let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .vertices() = (W1 .vertices()) \/ (W2 .vertices())
let W1, W2 be Walk of G; :: thesis: ( W1 .last() = W2 .first() implies (W1 .append W2) .vertices() = (W1 .vertices()) \/ (W2 .vertices()) )
set W = W1 .append W2;
assume A1: W1 .last() = W2 .first() ; :: thesis: (W1 .append W2) .vertices() = (W1 .vertices()) \/ (W2 .vertices())
then A2: W1 .append W2 = W1 ^' W2 by Def10;

now :: thesis: for x being object holds
( ( x in (W1 .append W2) .vertices() implies x in (W1 .vertices()) \/ (W2 .vertices()) ) & ( x in (W1 .vertices()) \/ (W2 .vertices()) implies x in (W1 .append W2) .vertices() ) )

let x be object ; :: thesis: ( ( x in (W1 .append W2) .vertices() implies x in (W1 .vertices()) \/ (W2 .vertices()) ) & ( x in (W1 .vertices()) \/ (W2 .vertices()) implies x in (W1 .append W2) .vertices() ) )

A3: now :: thesis: ( x in W1 .vertices() implies x in (W1 .append W2) .vertices() )

assume x in W1 .vertices() ; :: thesis: x in (W1 .append W2) .vertices()
then consider n being odd Element of NAT such that
A4: n <= len W1 and
A5: W1 . n = x by Lm45;
1 <= n by ABIAN:12;
then A6: n in dom W1 by A4, FINSEQ_3:25;
then n in dom (W1 .append W2) by Lm12;
then A7: n <= len (W1 .append W2) by FINSEQ_3:25;
(W1 .append W2) . n = x by A5, A6, Lm12;
hence x in (W1 .append W2) .vertices() by A7, Lm45; :: thesis: verum

end;

hereby :: thesis: ( x in (W1 .vertices()) \/ (W2 .vertices()) implies x in (W1 .append W2) .vertices() )

assume A8: x in (W1 .append W2) .vertices() ; :: thesis: x in (W1 .vertices()) \/ (W2 .vertices())
then reconsider v = x as Vertex of G ;
consider n being odd Element of NAT such that
A9: n <= len (W1 .append W2) and
A10: (W1 .append W2) . n = v by A8, Lm45;
A11: 1 <= n by ABIAN:12;

now :: thesis: x in (W1 .vertices()) \/ (W2 .vertices())

per cases ( n <= len W1 or n > len W1 ) ;

suppose A12: n <= len W1 ; :: thesis: x in (W1 .vertices()) \/ (W2 .vertices())

then n in dom W1 by A11, FINSEQ_3:25;
then W1 . n = v by A10, Lm12;
then v in W1 .vertices() by A12, Lm45;
hence x in (W1 .vertices()) \/ (W2 .vertices()) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A13: n > len W1 ; :: thesis: x in (W1 .vertices()) \/ (W2 .vertices())

then consider k being Nat such that
A14: (len W1) + k = n by NAT_1:10;
reconsider k = k as even Element of NAT by A14, ORDINAL1:def 12;
k <> 0 by A13, A14;
then A15: 0 + 1 <= k by NAT_1:13;
((len W1) + k) + 1 <= (len (W1 .append W2)) + 1 by A9, A14, XREAL_1:7;
then (k + 1) + (len W1) <= (len W2) + (len W1) by A1, Lm9;
then A16: ((k + 1) + (len W1)) - (len W1) <= ((len W2) + (len W1)) - (len W1) by XREAL_1:13;
then A17: W2 .vertexAt (k + 1) in W2 .vertices() by Th87;
k < ((len W2) - 1) + 1 by A16, NAT_1:13;
then W2 . (k + 1) = v by A2, A10, A14, A15, FINSEQ_6:141;
then v in W2 .vertices() by A16, A17, Def8;
hence x in (W1 .vertices()) \/ (W2 .vertices()) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in (W1 .vertices()) \/ (W2 .vertices()) ; :: thesis: verum

end;

assume A18: x in (W1 .vertices()) \/ (W2 .vertices()) ; :: thesis: x in (W1 .append W2) .vertices()

now :: thesis: x in (W1 .append W2) .vertices()

per cases ( x in W1 .vertices() or x in W2 .vertices() ) by A18, XBOOLE_0:def 3;

suppose x in W1 .vertices() ; :: thesis: x in (W1 .append W2) .vertices()

hence x in (W1 .append W2) .vertices() by A3; :: thesis: verum

end;

suppose A19: x in W2 .vertices() ; :: thesis: x in (W1 .append W2) .vertices()

reconsider lenW1 = len W1 as odd Element of NAT ;
consider n being odd Element of NAT such that
A20: n <= len W2 and
A21: W2 . n = x by A19, Lm45;
reconsider naa1 = n - 1 as even Element of NAT by ABIAN:12, INT_1:5;
A22: naa1 < (len W2) - 0 by A20, XREAL_1:15;
then (len W1) + naa1 in dom (W1 .append W2) by A1, Lm13;
then A23: lenW1 + naa1 <= len (W1 .append W2) by FINSEQ_3:25;
(W1 .append W2) . ((len W1) + naa1) = W2 . (naa1 + 1) by A1, A22, Lm13;
hence x in (W1 .append W2) .vertices() by A21, A23, Lm45; :: thesis: verum

end;

end;

end;

hence x in (W1 .append W2) .vertices() ; :: thesis: verum

end;

hence (W1 .append W2) .vertices() = (W1 .vertices()) \/ (W2 .vertices()) by TARSKI:2; :: thesis: verum