now

let y be set ; :: thesis: ( y in rng (W .weightSeq() ) implies y in REAL )
assume y in rng (W .weightSeq() ) ; :: thesis: y in REAL
then consider x being Nat such that
A1: x in dom (W .weightSeq() ) and
A2: y = (W .weightSeq() ) . x by FINSEQ_2:11;
( 1 <= x & x <= len (W .weightSeq() ) ) by A1, FINSEQ_3:27;
then y = (the_Weight_of G) . ((W .edgeSeq() ) . x) by A2, Def18;
hence y in REAL ; :: thesis: verum

end;

then rng (W .weightSeq() ) c= REAL by TARSKI:def 3;
hence W .weightSeq() is FinSequence of REAL by FINSEQ_1:def 4; :: thesis: verum