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

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