let G be WGraph; :: thesis: for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .weightSeq() = (W1 .weightSeq()) ^ (W2 .weightSeq())
let W1, W2 be Walk of G; :: thesis: ( W1 .last() = W2 .first() implies (W1 .append W2) .weightSeq() = (W1 .weightSeq()) ^ (W2 .weightSeq()) )
set W3 = W1 .append W2;
set W4 = (W1 .weightSeq()) ^ (W2 .weightSeq());
assume A1: W1 .last() = W2 .first() ; :: thesis: (W1 .append W2) .weightSeq() = (W1 .weightSeq()) ^ (W2 .weightSeq())
then (W1 .append W2) .edgeSeq() = (W1 .edgeSeq()) ^ (W2 .edgeSeq()) by GLIB_001:85;
then len ((W1 .append W2) .edgeSeq()) = (len (W1 .edgeSeq())) + (len (W2 .edgeSeq())) by FINSEQ_1:22;
then A2: len ((W1 .append W2) .weightSeq()) = (len (W1 .edgeSeq())) + (len (W2 .edgeSeq())) by Def18
.= (len (W1 .weightSeq())) + (len (W2 .edgeSeq())) by Def18
.= (len (W1 .weightSeq())) + (len (W2 .weightSeq())) by Def18
.= len ((W1 .weightSeq()) ^ (W2 .weightSeq())) by FINSEQ_1:22 ;

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

let n be Nat; :: thesis: ( 1 <= n & n <= len ((W1 .append W2) .weightSeq()) implies ((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . n )
assume A3: ( 1 <= n & n <= len ((W1 .append W2) .weightSeq()) ) ; :: thesis: ((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . n
then A4: ((W1 .append W2) .weightSeq()) . n = (the_Weight_of G) . (((W1 .append W2) .edgeSeq()) . n) by Def18
.= (the_Weight_of G) . (((W1 .edgeSeq()) ^ (W2 .edgeSeq())) . n) by A1, GLIB_001:85 ;
A5: n in dom ((W1 .weightSeq()) ^ (W2 .weightSeq())) by A2, A3, FINSEQ_3:25;

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

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

suppose A6: n in dom (W1 .weightSeq()) ; :: thesis: ((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . n

then A7: 1 <= n by FINSEQ_3:25;
A8: n <= len (W1 .weightSeq()) by A6, FINSEQ_3:25;
then n <= len (W1 .edgeSeq()) by Def18;
then A9: n in dom (W1 .edgeSeq()) by A7, FINSEQ_3:25;
((W1 .weightSeq()) ^ (W2 .weightSeq())) . n = (W1 .weightSeq()) . n by A6, FINSEQ_1:def 7
.= (the_Weight_of G) . ((W1 .edgeSeq()) . n) by A7, A8, Def18 ;
hence ((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . n by A4, A9, FINSEQ_1:def 7; :: thesis: verum

end;

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

then consider k being Nat such that
A10: k in dom (W2 .weightSeq()) and
A11: n = (len (W1 .weightSeq())) + k ;
A12: 1 <= k by A10, FINSEQ_3:25;
A13: k <= len (W2 .weightSeq()) by A10, FINSEQ_3:25;
then k <= len (W2 .edgeSeq()) by Def18;
then A14: k in dom (W2 .edgeSeq()) by A12, FINSEQ_3:25;
A15: n = (len (W1 .edgeSeq())) + k by A11, Def18;
((W1 .weightSeq()) ^ (W2 .weightSeq())) . n = (W2 .weightSeq()) . k by A10, A11, FINSEQ_1:def 7
.= (the_Weight_of G) . ((W2 .edgeSeq()) . k) by A12, A13, Def18 ;
hence ((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . n by A4, A14, A15, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

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

end;

hence (W1 .append W2) .weightSeq() = (W1 .weightSeq()) ^ (W2 .weightSeq()) by A2, FINSEQ_1:14; :: thesis: verum