let Omega be set ; :: thesis: for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Function of Sigma,REAL holds P * ASeq is Real_Sequence
let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma
for P being Function of Sigma,REAL holds P * ASeq is Real_Sequence
let ASeq be SetSequence of Sigma; :: thesis: for P being Function of Sigma,REAL holds P * ASeq is Real_Sequence
let P be Function of Sigma,REAL; :: thesis: P * ASeq is Real_Sequence
rng ASeq c= Sigma by RELAT_1:def 19;
then rng ASeq c= dom P by FUNCT_2:def 1;
then A1: dom (P * ASeq) = dom ASeq by RELAT_1:27
.= NAT by FUNCT_2:def 1 ;
rng (P * ASeq) c= REAL by RELAT_1:def 19;
hence P * ASeq is Real_Sequence by A1, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum