let G be real-weighted WGraph; for W1 being Walk of G
for W2 being Subwalk of W1 ex ws being Subset of (W1 .weightSeq()) st W2 .weightSeq() = Seq ws
let W1 be Walk of G; for W2 being Subwalk of W1 ex ws being Subset of (W1 .weightSeq()) st W2 .weightSeq() = Seq ws
let W2 be Subwalk of W1; ex ws being Subset of (W1 .weightSeq()) st W2 .weightSeq() = Seq ws
consider es being Subset of (W1 .edgeSeq()) such that
A1:
W2 .edgeSeq() = Seq es
by GLIB_001:def 32;
deffunc H1( object ) -> set = (the_Weight_of G) . (es . $1);
consider ws being Function such that
A2:
( dom ws = dom es & ( for x being object st x in dom es holds
ws . x = H1(x) ) )
from FUNCT_1:sch 3();
A3:
ex k being Nat st dom ws c= Seg k
by A2, FINSEQ_1:def 12;
then reconsider ws = ws as FinSubsequence by FINSEQ_1:def 12;
now for z being object st z in ws holds
z in W1 .weightSeq() let z be
object ;
( z in ws implies z in W1 .weightSeq() )assume A4:
z in ws
;
z in W1 .weightSeq() then consider x,
y being
object such that A5:
z = [x,y]
by RELAT_1:def 1;
A6:
x in dom es
by A2, A4, A5, FUNCT_1:1;
then A7:
[x,(es . x)] in es
by FUNCT_1:1;
then A8:
x in dom (W1 .edgeSeq())
by FUNCT_1:1;
A9:
ws . x = y
by A4, A5, FUNCT_1:1;
reconsider x =
x as
Element of
NAT by A8;
x <= len (W1 .edgeSeq())
by A8, FINSEQ_3:25;
then A10:
x <= len (W1 .weightSeq())
by Def18;
A11:
1
<= x
by A8, FINSEQ_3:25;
then A12:
(W1 .weightSeq()) . x = (the_Weight_of G) . ((W1 .edgeSeq()) . x)
by A10, Def18;
x in dom (W1 .weightSeq())
by A11, A10, FINSEQ_3:25;
then A13:
[x,((W1 .weightSeq()) . x)] in W1 .weightSeq()
by FUNCT_1:1;
y = (the_Weight_of G) . (es . x)
by A2, A6, A9;
hence
z in W1 .weightSeq()
by A5, A7, A13, A12, FUNCT_1:1;
verum end;
then reconsider ws = ws as Subset of (W1 .weightSeq()) by TARSKI:def 3;
take
ws
; W2 .weightSeq() = Seq ws
A14: len (Seq es) =
card es
by GLIB_001:5
.=
card (dom ws)
by A2, CARD_1:62
.=
card ws
by CARD_1:62
.=
len (Seq ws)
by GLIB_001:5
;
then A15:
len (W2 .weightSeq()) = len (Seq ws)
by A1, Def18;
now for n being Nat st 1 <= n & n <= len (W2 .weightSeq()) holds
(W2 .weightSeq()) . n = (Seq ws) . nA16:
rng (Sgm (dom es)) = dom es
by A2, A3, FINSEQ_1:def 13;
let n be
Nat;
( 1 <= n & n <= len (W2 .weightSeq()) implies (W2 .weightSeq()) . n = (Seq ws) . n )A17:
Seq ws = ws * (Sgm (dom es))
by A2, FINSEQ_1:def 14;
assume A18:
( 1
<= n &
n <= len (W2 .weightSeq()) )
;
(W2 .weightSeq()) . n = (Seq ws) . nthen A19:
(
Seq es = es * (Sgm (dom es)) &
n in dom (Seq es) )
by A14, A15, FINSEQ_1:def 14, FINSEQ_3:25;
A20:
n in dom (Seq ws)
by A15, A18, FINSEQ_3:25;
then
n in dom (Sgm (dom es))
by A17, FUNCT_1:11;
then A21:
(Sgm (dom es)) . n in dom es
by A16, FUNCT_1:def 3;
(Seq ws) . n =
ws . ((Sgm (dom es)) . n)
by A17, A20, FUNCT_1:12
.=
(the_Weight_of G) . (es . ((Sgm (dom es)) . n))
by A2, A21
.=
(the_Weight_of G) . ((Seq es) . n)
by A19, FUNCT_1:12
;
hence
(W2 .weightSeq()) . n = (Seq ws) . n
by A1, A18, Def18;
verum end;
hence
W2 .weightSeq() = Seq ws
by A15, FINSEQ_1:14; verum