let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 .last() = W2 .first() holds

(W1 .append W2) .edges() = (W1 .edges()) \/ (W2 .edges())

let W1, W2 be Walk of G; :: thesis: ( W1 .last() = W2 .first() implies (W1 .append W2) .edges() = (W1 .edges()) \/ (W2 .edges()) )

set W = W1 .append W2;

set WE = (W1 .append W2) .edges() ;

set W1E = W1 .edges() ;

set W2E = W2 .edges() ;

set lenW1 = len W1;

set lenW2 = len W2;

reconsider lenW1 = len W1, lenW2 = len W2 as odd Element of NAT ;

assume A1: W1 .last() = W2 .first() ; :: thesis: (W1 .append W2) .edges() = (W1 .edges()) \/ (W2 .edges())

then A2: W1 .append W2 = W1 ^' W2 by Def10;

(W1 .append W2) .edges() = (W1 .edges()) \/ (W2 .edges())

let W1, W2 be Walk of G; :: thesis: ( W1 .last() = W2 .first() implies (W1 .append W2) .edges() = (W1 .edges()) \/ (W2 .edges()) )

set W = W1 .append W2;

set WE = (W1 .append W2) .edges() ;

set W1E = W1 .edges() ;

set W2E = W2 .edges() ;

set lenW1 = len W1;

set lenW2 = len W2;

reconsider lenW1 = len W1, lenW2 = len W2 as odd Element of NAT ;

assume A1: W1 .last() = W2 .first() ; :: thesis: (W1 .append W2) .edges() = (W1 .edges()) \/ (W2 .edges())

then A2: W1 .append W2 = W1 ^' W2 by Def10;

now :: thesis: for x being object holds

( ( x in (W1 .append W2) .edges() implies x in (W1 .edges()) \/ (W2 .edges()) ) & ( x in (W1 .edges()) \/ (W2 .edges()) implies x in (W1 .append W2) .edges() ) )

hence
(W1 .append W2) .edges() = (W1 .edges()) \/ (W2 .edges())
by TARSKI:2; :: thesis: verum( ( x in (W1 .append W2) .edges() implies x in (W1 .edges()) \/ (W2 .edges()) ) & ( x in (W1 .edges()) \/ (W2 .edges()) implies x in (W1 .append W2) .edges() ) )

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

end;hereby :: thesis: ( x in (W1 .edges()) \/ (W2 .edges()) implies x in (W1 .append W2) .edges() )

assume A10:
x in (W1 .edges()) \/ (W2 .edges())
; :: thesis: x in (W1 .append W2) .edges() assume
x in (W1 .append W2) .edges()
; :: thesis: x in (W1 .edges()) \/ (W2 .edges())

then consider n being even Element of NAT such that

A3: 1 <= n and

A4: n <= len (W1 .append W2) and

A5: (W1 .append W2) . n = x by Lm46;

end;then consider n being even Element of NAT such that

A3: 1 <= n and

A4: n <= len (W1 .append W2) and

A5: (W1 .append W2) . n = x by Lm46;

now :: thesis: x in (W1 .edges()) \/ (W2 .edges())end;

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

end;

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

then
(W1 .append W2) . n = W1 . n
by A2, A3, FINSEQ_6:140;

then x in W1 .edges() by A3, A5, A6, Lm46;

hence x in (W1 .edges()) \/ (W2 .edges()) by XBOOLE_0:def 3; :: thesis: verum

end;then x in W1 .edges() by A3, A5, A6, Lm46;

hence x in (W1 .edges()) \/ (W2 .edges()) by XBOOLE_0:def 3; :: thesis: verum

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

then reconsider k = n - lenW1 as odd Element of NAT by INT_1:5;

A7: 1 <= k + 1 by NAT_1:12;

(n - lenW1) + (len W1) < (len (W1 .append W2)) + 1 by A4, NAT_1:13;

then (n - lenW1) + lenW1 < lenW2 + (len W1) by A1, Lm9;

then A8: k < (lenW2 + (len W1)) - (len W1) by XREAL_1:14;

then A9: k + 1 <= len W2 by NAT_1:13;

W2 . (k + 1) = (W1 .append W2) . ((len W1) + k) by A2, A8, ABIAN:12, FINSEQ_6:141

.= x by A5 ;

then x in W2 .edges() by A7, A9, Lm46;

hence x in (W1 .edges()) \/ (W2 .edges()) by XBOOLE_0:def 3; :: thesis: verum

end;A7: 1 <= k + 1 by NAT_1:12;

(n - lenW1) + (len W1) < (len (W1 .append W2)) + 1 by A4, NAT_1:13;

then (n - lenW1) + lenW1 < lenW2 + (len W1) by A1, Lm9;

then A8: k < (lenW2 + (len W1)) - (len W1) by XREAL_1:14;

then A9: k + 1 <= len W2 by NAT_1:13;

W2 . (k + 1) = (W1 .append W2) . ((len W1) + k) by A2, A8, ABIAN:12, FINSEQ_6:141

.= x by A5 ;

then x in W2 .edges() by A7, A9, Lm46;

hence x in (W1 .edges()) \/ (W2 .edges()) by XBOOLE_0:def 3; :: thesis: verum

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

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

end;

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

then consider n being even Element of NAT such that

A11: 1 <= n and

A12: n <= len W1 and

A13: W1 . n = x by Lm46;

len W1 <= len (W1 .append W2) by A1, Lm10;

then A14: n <= len (W1 .append W2) by A12, XXREAL_0:2;

(W1 .append W2) . n = x by A2, A11, A12, A13, FINSEQ_6:140;

hence x in (W1 .append W2) .edges() by A11, A14, Lm46; :: thesis: verum

end;A11: 1 <= n and

A12: n <= len W1 and

A13: W1 . n = x by Lm46;

len W1 <= len (W1 .append W2) by A1, Lm10;

then A14: n <= len (W1 .append W2) by A12, XXREAL_0:2;

(W1 .append W2) . n = x by A2, A11, A12, A13, FINSEQ_6:140;

hence x in (W1 .append W2) .edges() by A11, A14, Lm46; :: thesis: verum

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

then consider n being even Element of NAT such that

A15: 1 <= n and

A16: n <= len W2 and

A17: W2 . n = x by Lm46;

reconsider naa1 = n - 1 as odd Element of NAT by A15, INT_1:5;

naa1 < len W2 by A16, XREAL_1:147;

then A18: (W1 .append W2) . (lenW1 + naa1) = W2 . (naa1 + 1) by A2, ABIAN:12, FINSEQ_6:141

.= x by A17 ;

(naa1 + 1) + lenW1 <= (len W2) + (len W1) by A16, XREAL_1:7;

then (lenW1 + naa1) + 1 <= (len (W1 .append W2)) + 1 by A1, Lm9;

then A19: lenW1 + naa1 <= len (W1 .append W2) by XREAL_1:6;

1 <= lenW1 + naa1 by ABIAN:12, NAT_1:12;

hence x in (W1 .append W2) .edges() by A18, A19, Lm46; :: thesis: verum

end;A15: 1 <= n and

A16: n <= len W2 and

A17: W2 . n = x by Lm46;

reconsider naa1 = n - 1 as odd Element of NAT by A15, INT_1:5;

naa1 < len W2 by A16, XREAL_1:147;

then A18: (W1 .append W2) . (lenW1 + naa1) = W2 . (naa1 + 1) by A2, ABIAN:12, FINSEQ_6:141

.= x by A17 ;

(naa1 + 1) + lenW1 <= (len W2) + (len W1) by A16, XREAL_1:7;

then (lenW1 + naa1) + 1 <= (len (W1 .append W2)) + 1 by A1, Lm9;

then A19: lenW1 + naa1 <= len (W1 .append W2) by XREAL_1:6;

1 <= lenW1 + naa1 by ABIAN:12, NAT_1:12;

hence x in (W1 .append W2) .edges() by A18, A19, Lm46; :: thesis: verum