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;

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

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

hereby :: thesis: ( x in (W1 .edges()) \/ (W2 .edges()) implies 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;

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

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

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;

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;

end;

end;

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

end;

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

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

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

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;

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;

end;

end;

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

end;

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