let D be non empty set ; :: thesis: for r being Real
for H being Functional_Sequence of D,REAL
for X being set st X common_on_dom H holds
X common_on_dom r (#) H
let r be Real; :: thesis: for H being Functional_Sequence of D,REAL
for X being set st X common_on_dom H holds
X common_on_dom r (#) H
let H be Functional_Sequence of D,REAL; :: thesis: for X being set st X common_on_dom H holds
X common_on_dom r (#) H
let X be set ; :: thesis: ( X common_on_dom H implies X common_on_dom r (#) H )
assume A1: X common_on_dom H ; :: thesis: X common_on_dom r (#) H
A2: now :: thesis: for n being Nat holds X c= dom ((r (#) H) . n)
let n be Nat; :: thesis: X c= dom ((r (#) H) . n)
dom (H . n) = dom (r (#) (H . n)) by VALUED_1:def 5
.= dom ((r (#) H) . n) by Def1 ;
hence X c= dom ((r (#) H) . n) by A1; :: thesis: verum
end;
X <> {} by A1;
hence X common_on_dom r (#) H by A2; :: thesis: verum