now :: thesis: for y being object st y in rng (W .weightSeq()) holds
y in REAL
let y be object ; :: 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:10;
( 1 <= x & x <= len (W .weightSeq()) ) by A1, FINSEQ_3:25;
then y = (the_Weight_of G) . ((W .edgeSeq()) . x) by A2, Def18;
hence y in REAL by XREAL_0:def 1; :: 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