let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .edgeSeq() = (W1 .edgeSeq()) ^ (W2 .edgeSeq())
let W1, W2 be Walk of G; :: thesis: ( W1 .last() = W2 .first() implies (W1 .append W2) .edgeSeq() = (W1 .edgeSeq()) ^ (W2 .edgeSeq()) )
set W3 = W1 .append W2;
set W4 = (W1 .edgeSeq()) ^ (W2 .edgeSeq());
A1: len ((W1 .edgeSeq()) ^ (W2 .edgeSeq())) = (len (W1 .edgeSeq())) + (len (W2 .edgeSeq())) by FINSEQ_1:22;
assume A2: W1 .last() = W2 .first() ; :: thesis: (W1 .append W2) .edgeSeq() = (W1 .edgeSeq()) ^ (W2 .edgeSeq())
then (len (W1 .append W2)) + 1 = (len W1) + (len W2) by Lm9;
then (len (W1 .append W2)) + 1 = (len W1) + ((2 * (len (W2 .edgeSeq()))) + 1) by Def15
.= ((len W1) + (2 * (len (W2 .edgeSeq())))) + 1 ;
then A3: (2 * (len ((W1 .append W2) .edgeSeq()))) + 1 = (2 * (len (W2 .edgeSeq()))) + (len W1) by Def15
.= (2 * (len (W2 .edgeSeq()))) + ((2 * (len (W1 .edgeSeq()))) + 1) by Def15
.= ((2 * (len (W2 .edgeSeq()))) + (2 * (len (W1 .edgeSeq())))) + 1 ;
A4: W1 .append W2 = W1 ^' W2 by A2, Def10;

now :: thesis: for n being Nat st 1 <= n & n <= len ((W1 .append W2) .edgeSeq()) holds
((W1 .append W2) .edgeSeq()) . n = ((W1 .edgeSeq()) ^ (W2 .edgeSeq())) . n

let n be Nat; :: thesis: ( 1 <= n & n <= len ((W1 .append W2) .edgeSeq()) implies ((W1 .append W2) .edgeSeq()) . n = ((W1 .edgeSeq()) ^ (W2 .edgeSeq())) . n )
assume that
A5: 1 <= n and
A6: n <= len ((W1 .append W2) .edgeSeq()) ; :: thesis: ((W1 .append W2) .edgeSeq()) . n = ((W1 .edgeSeq()) ^ (W2 .edgeSeq())) . n
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
A7: ((W1 .append W2) .edgeSeq()) . n1 = (W1 .append W2) . (2 * n1) by A5, A6, Def15;
A8: n1 in dom ((W1 .edgeSeq()) ^ (W2 .edgeSeq())) by A1, A3, A5, A6, FINSEQ_3:25;

now :: thesis: ((W1 .append W2) .edgeSeq()) . n = ((W1 .edgeSeq()) ^ (W2 .edgeSeq())) . n

per cases ( n in dom (W1 .edgeSeq()) or ex k being Nat st
( k in dom (W2 .edgeSeq()) & n = (len (W1 .edgeSeq())) + k ) ) by A8, FINSEQ_1:25;

suppose A9: n in dom (W1 .edgeSeq()) ; :: thesis: ((W1 .append W2) .edgeSeq()) . n = ((W1 .edgeSeq()) ^ (W2 .edgeSeq())) . n

then A10: n <= len (W1 .edgeSeq()) by FINSEQ_3:25;
A11: 1 <= n by A9, FINSEQ_3:25;
A12: 2 * n in dom W1 by A9, Lm41;
then A13: 1 <= 2 * n by FINSEQ_3:25;
A14: 2 * n <= len W1 by A12, FINSEQ_3:25;
((W1 .edgeSeq()) ^ (W2 .edgeSeq())) . n = (W1 .edgeSeq()) . n by A9, FINSEQ_1:def 7
.= W1 . (2 * n) by A11, A10, Def15 ;
hence ((W1 .append W2) .edgeSeq()) . n = ((W1 .edgeSeq()) ^ (W2 .edgeSeq())) . n by A4, A7, A13, A14, FINSEQ_6:140; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom (W2 .edgeSeq()) & n = (len (W1 .edgeSeq())) + k ) ; :: thesis: ((W1 .append W2) .edgeSeq()) . n = ((W1 .edgeSeq()) ^ (W2 .edgeSeq())) . n

then consider k being Nat such that
A15: k in dom (W2 .edgeSeq()) and
A16: n = (len (W1 .edgeSeq())) + k ;
(2 * n) + 1 = (2 * k) + ((2 * (len (W1 .edgeSeq()))) + 1) by A16
.= (2 * k) + (len W1) by Def15 ;
then A17: 2 * n = (len W1) + ((2 * k) - 1) ;
A18: 1 <= k by A15, FINSEQ_3:25;
then 1 <= k + k by NAT_1:12;
then reconsider 2kaa1 = (2 * k) - 1 as Element of NAT by INT_1:5;
A19: k <= len (W2 .edgeSeq()) by A15, FINSEQ_3:25;
then 2 * k <= 2 * (len (W2 .edgeSeq())) by XREAL_1:64;
then 2 * k < (2 * (len (W2 .edgeSeq()))) + 1 by NAT_1:13;
then 2 * k < len W2 by Def15;
then A20: 2kaa1 < (len W2) - 0 by XREAL_1:14;
1 + 1 <= k + k by A18, XREAL_1:7;
then (1 + 1) - 1 <= 2kaa1 by XREAL_1:13;
then A21: (W1 .append W2) . (2 * n) = W2 . (2kaa1 + 1) by A4, A17, A20, FINSEQ_6:141
.= W2 . (2 * k) ;
((W1 .edgeSeq()) ^ (W2 .edgeSeq())) . n = (W2 .edgeSeq()) . k by A15, A16, FINSEQ_1:def 7
.= W2 . (2 * k) by A18, A19, Def15 ;
hence ((W1 .append W2) .edgeSeq()) . n = ((W1 .edgeSeq()) ^ (W2 .edgeSeq())) . n by A5, A6, A21, Def15; :: thesis: verum

end;

end;

end;

hence ((W1 .append W2) .edgeSeq()) . n = ((W1 .edgeSeq()) ^ (W2 .edgeSeq())) . n ; :: thesis: verum

end;

hence (W1 .append W2) .edgeSeq() = (W1 .edgeSeq()) ^ (W2 .edgeSeq()) by A1, A3, FINSEQ_1:14; :: thesis: verum