let G1 be WGraph; for G2 being WSubgraph of G1
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .weightSeq() = W2 .weightSeq()
let G2 be WSubgraph of G1; for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .weightSeq() = W2 .weightSeq()
let W1 be Walk of G1; for W2 being Walk of G2 st W1 = W2 holds
W1 .weightSeq() = W2 .weightSeq()
let W2 be Walk of G2; ( W1 = W2 implies W1 .weightSeq() = W2 .weightSeq() )
set WS1 = W1 .weightSeq() ;
set WS2 = W2 .weightSeq() ;
assume
W1 = W2
; W1 .weightSeq() = W2 .weightSeq()
then A1:
W1 .edgeSeq() = W2 .edgeSeq()
by GLIB_001:86;
now ( len (W1 .weightSeq()) = len (W1 .weightSeq()) & len (W2 .weightSeq()) = len (W1 .weightSeq()) & ( for x being Nat st x in dom (W1 .weightSeq()) holds
(W2 .weightSeq()) . x = (W1 .weightSeq()) . x ) )thus
len (W1 .weightSeq()) = len (W1 .weightSeq())
;
( len (W2 .weightSeq()) = len (W1 .weightSeq()) & ( for x being Nat st x in dom (W1 .weightSeq()) holds
(W2 .weightSeq()) . x = (W1 .weightSeq()) . x ) )thus A2:
len (W2 .weightSeq()) =
len (W1 .edgeSeq())
by A1, Def18
.=
len (W1 .weightSeq())
by Def18
;
for x being Nat st x in dom (W1 .weightSeq()) holds
(W2 .weightSeq()) . x = (W1 .weightSeq()) . xlet x be
Nat;
( x in dom (W1 .weightSeq()) implies (W2 .weightSeq()) . x = (W1 .weightSeq()) . x )assume A3:
x in dom (W1 .weightSeq())
;
(W2 .weightSeq()) . x = (W1 .weightSeq()) . xthen A4:
1
<= x
by FINSEQ_3:25;
A5:
x <= len (W2 .weightSeq())
by A2, A3, FINSEQ_3:25;
then
x <= len (W2 .edgeSeq())
by Def18;
then A6:
x in dom (W2 .edgeSeq())
by A4, FINSEQ_3:25;
A7:
x <= len (W1 .weightSeq())
by A3, FINSEQ_3:25;
thus (W2 .weightSeq()) . x =
(the_Weight_of G2) . ((W2 .edgeSeq()) . x)
by A4, A5, Def18
.=
((the_Weight_of G1) | (the_Edges_of G2)) . ((W2 .edgeSeq()) . x)
by Def10
.=
(the_Weight_of G1) . ((W1 .edgeSeq()) . x)
by A1, A6, FUNCT_1:49, GLIB_001:79
.=
(W1 .weightSeq()) . x
by A4, A7, Def18
;
verum end;
hence
W1 .weightSeq() = W2 .weightSeq()
by FINSEQ_2:9; verum