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