let G1 be WGraph; :: thesis: 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; :: thesis: 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; :: thesis: for W2 being Walk of G2 st W1 = W2 holds
W1 .weightSeq() = W2 .weightSeq()
let W2 be Walk of G2; :: thesis: ( W1 = W2 implies W1 .weightSeq() = W2 .weightSeq() )
set WS1 = W1 .weightSeq() ;
set WS2 = W2 .weightSeq() ;
assume W1 = W2 ; :: thesis: W1 .weightSeq() = W2 .weightSeq()
then A1: W1 .edgeSeq() = W2 .edgeSeq() by GLIB_001:86;

now :: thesis: ( 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()) ; :: thesis: ( 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 ; :: thesis: for x being Nat st x in dom (W1 .weightSeq()) holds
(W2 .weightSeq()) . x = (W1 .weightSeq()) . x
let x be Nat; :: thesis: ( x in dom (W1 .weightSeq()) implies (W2 .weightSeq()) . x = (W1 .weightSeq()) . x )
assume A3: x in dom (W1 .weightSeq()) ; :: thesis: (W2 .weightSeq()) . x = (W1 .weightSeq()) . x
then 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 ; :: thesis: verum

end;

hence W1 .weightSeq() = W2 .weightSeq() by FINSEQ_2:9; :: thesis: verum