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:86;
then len ((W1 .append W2) .edgeSeq() ) = (len (W1 .edgeSeq() )) + (len (W2 .edgeSeq() )) by FINSEQ_1:35;
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:35 ;

now

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:86 ;
A5: n in dom ((W1 .weightSeq() ) ^ (W2 .weightSeq() )) by A2, A3, FINSEQ_3:27;

now

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:38;

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:27;
A8: n <= len (W1 .weightSeq() ) by A6, FINSEQ_3:27;
then n <= len (W1 .edgeSeq() ) by Def18;
then A9: n in dom (W1 .edgeSeq() ) by A7, FINSEQ_3:27;
((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:27;
A13: k <= len (W2 .weightSeq() ) by A10, FINSEQ_3:27;
then k <= len (W2 .edgeSeq() ) by Def18;
then A14: k in dom (W2 .edgeSeq() ) by A12, FINSEQ_3:27;
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:18; :: thesis: verum