let X be set ; :: thesis: for F being Field_Subset of X
for FSets being Set_Sequence of F
for M being Function of F,ExtREAL holds M * FSets is ExtREAL_sequence
let F be Field_Subset of X; :: thesis: for FSets being Set_Sequence of F
for M being Function of F,ExtREAL holds M * FSets is ExtREAL_sequence
let FSets be Set_Sequence of F; :: thesis: for M being Function of F,ExtREAL holds M * FSets is ExtREAL_sequence
let M be Function of F,ExtREAL ; :: thesis: M * FSets is ExtREAL_sequence

now

let y be set ; :: thesis: ( y in rng FSets implies y in F )
assume y in rng FSets ; :: thesis: y in F
then ex x being set st
( x in NAT & FSets . x = y ) by FUNCT_2:17;
hence y in F by DDef4; :: thesis: verum

end;

then rng FSets c= F by TARSKI:def 3;
then rng FSets c= dom M by FUNCT_2:def 1;
then dom (M * FSets) = dom FSets by RELAT_1:46;
then dom (M * FSets) = NAT by FUNCT_2:def 1;
hence M * FSets is ExtREAL_sequence by FUNCT_2:def 1; :: thesis: verum