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;

(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() ) )

hence
(W1 .append W2) .vertices() = (W1 .vertices()) \/ (W2 .vertices())
by TARSKI:2; :: thesis: verum( ( 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() ) )

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

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

assume A18:
x in (W1 .vertices()) \/ (W2 .vertices())
; :: thesis: 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;

end;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())end;

hence
x in (W1 .vertices()) \/ (W2 .vertices())
; :: thesis: verumper cases
( n <= len W1 or n > len W1 )
;

end;

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

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

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

hence
x in (W1 .append W2) .vertices()
; :: thesis: verumper cases
( x in W1 .vertices() or x in W2 .vertices() )
by A18, XBOOLE_0:def 3;

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