let X be set ; :: thesis: for S being SigmaField of X
for SSets being SetSequence of S
for M being Function of S,ExtREAL holds M * SSets is ExtREAL_sequence
let S be SigmaField of X; :: thesis: for SSets being SetSequence of S
for M being Function of S,ExtREAL holds M * SSets is ExtREAL_sequence
let SSets be SetSequence of S; :: thesis: for M being Function of S,ExtREAL holds M * SSets is ExtREAL_sequence
let M be Function of S,ExtREAL; :: thesis: M * SSets is ExtREAL_sequence
rng SSets c= S ;
then rng SSets c= dom M by FUNCT_2:def 1;
then dom (M * SSets) = dom SSets by RELAT_1:27;
then dom (M * SSets) = NAT by FUNCT_2:def 1;
hence M * SSets is ExtREAL_sequence by FUNCT_2:def 1; :: thesis: verum