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

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

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

then
rng FSets c= F
;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;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

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