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 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 ;
then (n - lenW1) + lenW1 < lenW2 + (len W1) by ;
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
.= 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 ;
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 ;
then A14: n <= len (W1 .append W2) by ;
(W1 .append W2) . n = x by ;
hence x in (W1 .append W2) .edges() by ; :: 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 ;
naa1 < len W2 by ;
then A18: (W1 .append W2) . (lenW1 + naa1) = W2 . (naa1 + 1) by
.= x by A17 ;
(naa1 + 1) + lenW1 <= (len W2) + (len W1) by ;
then (lenW1 + naa1) + 1 <= (len (W1 .append W2)) + 1 by ;
then A19: lenW1 + naa1 <= len (W1 .append W2) by XREAL_1:6;
1 <= lenW1 + naa1 by ;
hence x in (W1 .append W2) .edges() by ; :: 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