let G be real-weighted WGraph; :: thesis: 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; :: thesis: for W2 being Subwalk of W1 ex ws being Subset of (W1 .weightSeq()) st W2 .weightSeq() = Seq ws
let W2 be Subwalk of W1; :: thesis: 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 H₁( 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 = H₁(x) ) ) from FUNCT_1:sch 3();
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 :: thesis: for z being object st z in ws holds
z in W1 .weightSeq()

let z be object ; :: thesis: ( z in ws implies z in W1 .weightSeq() )
assume A4: z in ws ; :: thesis: 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; :: thesis: verum

end;

then reconsider ws = ws as Subset of (W1 .weightSeq()) by TARSKI:def 3;
take ws ; :: thesis: 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 :: thesis: for n being Nat st 1 <= n & n <= len (W2 .weightSeq()) holds
(W2 .weightSeq()) . n = (Seq ws) . n

A16: rng (Sgm (dom es)) = dom es by FINSEQ_1:def 14;
let n be Nat; :: thesis: ( 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 15;
assume A18: ( 1 <= n & n <= len (W2 .weightSeq()) ) ; :: thesis: (W2 .weightSeq()) . n = (Seq ws) . n
then A19: ( Seq es = es * (Sgm (dom es)) & n in dom (Seq es) ) by A14, A15, FINSEQ_1:def 15, 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; :: thesis: verum

end;

hence W2 .weightSeq() = Seq ws by A15, FINSEQ_1:14; :: thesis: verum