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

let W1, W2 be Walk of G; :: thesis: ( W1 .last() = W2 .first() implies (W1 .append W2) .edgeSeq() = () ^ () )
set W3 = W1 .append W2;
set W4 = () ^ ();
A1: len (() ^ ()) = (len ()) + (len ()) by FINSEQ_1:22;
assume A2: W1 .last() = W2 .first() ; :: thesis: (W1 .append W2) .edgeSeq() = () ^ ()
then (len (W1 .append W2)) + 1 = (len W1) + (len W2) by Lm9;
then (len (W1 .append W2)) + 1 = (len W1) + ((2 * (len ())) + 1) by Def15
.= ((len W1) + (2 * (len ()))) + 1 ;
then A3: (2 * (len ((W1 .append W2) .edgeSeq()))) + 1 = (2 * (len ())) + (len W1) by Def15
.= (2 * (len ())) + ((2 * (len ())) + 1) by Def15
.= ((2 * (len ())) + (2 * (len ()))) + 1 ;
A4: W1 .append W2 = W1 ^' W2 by ;
now :: thesis: for n being Nat st 1 <= n & n <= len ((W1 .append W2) .edgeSeq()) holds
((W1 .append W2) .edgeSeq()) . n = (() ^ ()) . n
let n be Nat; :: thesis: ( 1 <= n & n <= len ((W1 .append W2) .edgeSeq()) implies ((W1 .append W2) .edgeSeq()) . n = (() ^ ()) . n )
assume that
A5: 1 <= n and
A6: n <= len ((W1 .append W2) .edgeSeq()) ; :: thesis: ((W1 .append W2) .edgeSeq()) . n = (() ^ ()) . n
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
A7: ((W1 .append W2) .edgeSeq()) . n1 = (W1 .append W2) . (2 * n1) by ;
A8: n1 in dom (() ^ ()) by ;
now :: thesis: ((W1 .append W2) .edgeSeq()) . n = (() ^ ()) . n
per cases ( n in dom () or ex k being Nat st
( k in dom () & n = (len ()) + k ) )
by ;
suppose A9: n in dom () ; :: thesis: ((W1 .append W2) .edgeSeq()) . n = (() ^ ()) . n
then A10: n <= len () by FINSEQ_3:25;
A11: 1 <= n by ;
A12: 2 * n in dom W1 by ;
then A13: 1 <= 2 * n by FINSEQ_3:25;
A14: 2 * n <= len W1 by ;
(() ^ ()) . n = () . n by
.= W1 . (2 * n) by ;
hence ((W1 .append W2) .edgeSeq()) . n = (() ^ ()) . n by ; :: thesis: verum
end;
suppose ex k being Nat st
( k in dom () & n = (len ()) + k ) ; :: thesis: ((W1 .append W2) .edgeSeq()) . n = (() ^ ()) . n
then consider k being Nat such that
A15: k in dom () and
A16: n = (len ()) + k ;
(2 * n) + 1 = (2 * k) + ((2 * (len ())) + 1) by A16
.= (2 * k) + (len W1) by Def15 ;
then A17: 2 * n = (len W1) + ((2 * k) - 1) ;
A18: 1 <= k by ;
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 () by ;
then 2 * k <= 2 * (len ()) by XREAL_1:64;
then 2 * k < (2 * (len ())) + 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 ;
then (1 + 1) - 1 <= 2kaa1 by XREAL_1:13;
then A21: (W1 .append W2) . (2 * n) = W2 . (2kaa1 + 1) by
.= W2 . (2 * k) ;
(() ^ ()) . n = () . k by
.= W2 . (2 * k) by ;
hence ((W1 .append W2) .edgeSeq()) . n = (() ^ ()) . n by A5, A6, A21, Def15; :: thesis: verum
end;
end;
end;
hence ((W1 .append W2) .edgeSeq()) . n = (() ^ ()) . n ; :: thesis: verum
end;
hence (W1 .append W2) .edgeSeq() = () ^ () by ; :: thesis: verum