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 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