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 :: thesis: for y being object st y in rng FSets holds
y in F
let y be object ; :: thesis: ( y in rng FSets implies y in F )
assume y in rng FSets ; :: thesis: y in F
then ex x being object st
( x in NAT & FSets . x = y ) by FUNCT_2:11;
hence y in F by Def2; :: thesis: verum
end;
then rng FSets c= F ;
then rng FSets c= dom M by FUNCT_2:def 1;
then dom (M * FSets) = dom FSets by RELAT_1:27;
then dom (M * FSets) = NAT by FUNCT_2:def 1;
hence M * FSets is ExtREAL_sequence by FUNCT_2:def 1; :: thesis: verum