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

let x be set ; :: 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() ) )

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

assume A3: 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
A4: ( n <= len (W1 .append W2) & (W1 .append W2) . n = v ) by A3, Lm45;
A5: 1 <= n by HEYTING3:1;

now

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

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

then n in dom W1 by A5, FINSEQ_3:27;
then W1 . n = v by A4, Lm12;
then v in W1 .vertices() by A6, Lm45;
hence x in (W1 .vertices() ) \/ (W2 .vertices() ) by XBOOLE_0:def 3; :: thesis: verum

end;

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

then consider k being Nat such that
A8: (len W1) + k = n by NAT_1:10;
reconsider lenW1 = len W1 as odd Element of NAT ;
k is even by A8;
then reconsider k = k as even Element of NAT by ORDINAL1:def 13;
k <> 0 by A7, A8;
then 0 < k ;
then A9: 0 + 1 <= k by NAT_1:13;
((len W1) + k) + 1 <= (len (W1 .append W2)) + 1 by A4, A8, XREAL_1:9;
then (k + 1) + (len W1) <= (len W2) + (len W1) by A1, Lm9;
then A10: ((k + 1) + (len W1)) - (len W1) <= ((len W2) + (len W1)) - (len W1) by XREAL_1:15;
then k < ((len W2) - 1) + 1 by NAT_1:13;
then A11: W2 . (k + 1) = v by A2, A4, A8, A9, GRAPH_2:15;
W2 .vertexAt (k + 1) in W2 .vertices() by A10, Th90;
then v in W2 .vertices() by A10, A11, 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 A12: x in (W1 .vertices() ) \/ (W2 .vertices() ) ; :: thesis: x in (W1 .append W2) .vertices()

A13: now

assume x in W1 .vertices() ; :: thesis: x in (W1 .append W2) .vertices()
then consider n being odd Element of NAT such that
A14: ( n <= len W1 & W1 . n = x ) by Lm45;
1 <= n by HEYTING3:1;
then n in dom W1 by A14, FINSEQ_3:27;
then ( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) ) by Lm12;
then ( (W1 .append W2) . n = x & n <= len (W1 .append W2) ) by A14, FINSEQ_3:27;
hence x in (W1 .append W2) .vertices() by Lm45; :: thesis: verum

end;

now

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

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

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

end;

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

then consider n being odd Element of NAT such that
A15: ( n <= len W2 & W2 . n = x ) by Lm45;
reconsider naa1 = n - 1 as even Element of NAT by HEYTING3:1, INT_1:18;
naa1 < (len W2) - 0 by A15, XREAL_1:17;
then A16: ( (W1 .append W2) . ((len W1) + naa1) = W2 . (naa1 + 1) & (len W1) + naa1 in dom (W1 .append W2) ) by A1, Lm13;
reconsider lenW1 = len W1 as odd Element of NAT ;
lenW1 + naa1 <= len (W1 .append W2) by A16, FINSEQ_3:27;
hence x in (W1 .append W2) .vertices() by A15, A16, 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