let G be WGraph; 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; ( 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()
; (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 for n being Nat st 1 <= n & n <= len ((W1 .append W2) .weightSeq()) holds
((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . nlet n be
Nat;
( 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()) )
;
((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . nthen 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 ((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . nper 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 )
;
((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . nthen 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;
verum end; end; end; hence
((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . n
;
verum end;
hence
(W1 .append W2) .weightSeq() = (W1 .weightSeq()) ^ (W2 .weightSeq())
by A2, FINSEQ_1:14; verum