let G be _Graph; 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; ( W1 .last() = W2 .first() implies (W1 .append W2) .vertices() = (W1 .vertices()) \/ (W2 .vertices()) )
set W = W1 .append W2;
assume A1:
W1 .last() = W2 .first()
; (W1 .append W2) .vertices() = (W1 .vertices()) \/ (W2 .vertices())
then A2:
W1 .append W2 = W1 ^' W2
by Def10;
now 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 ;
( ( 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 ( x in (W1 .vertices()) \/ (W2 .vertices()) implies x in (W1 .append W2) .vertices() )
assume A8:
x in (W1 .append W2) .vertices()
;
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 x in (W1 .vertices()) \/ (W2 .vertices())per cases
( n <= len W1 or n > len W1 )
;
suppose A13:
n > len W1
;
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;
verum end; end; end; hence
x in (W1 .vertices()) \/ (W2 .vertices())
;
verum
end; assume A18:
x in (W1 .vertices()) \/ (W2 .vertices())
;
x in (W1 .append W2) .vertices() hence
x in (W1 .append W2) .vertices()
;
verum end;
hence
(W1 .append W2) .vertices() = (W1 .vertices()) \/ (W2 .vertices())
by TARSKI:2; verum