let D be non empty set ; :: thesis: for H being Functional_Sequence of D,REAL
for X being set st X common_on_dom H holds
for x being Element of D st x in X holds
{x} common_on_dom H
let H be Functional_Sequence of D,REAL; :: thesis: for X being set st X common_on_dom H holds
for x being Element of D st x in X holds
{x} common_on_dom H
let X be set ; :: thesis: ( X common_on_dom H implies for x being Element of D st x in X holds
{x} common_on_dom H )
assume A1: X common_on_dom H ; :: thesis: for x being Element of D st x in X holds
{x} common_on_dom H
let x be Element of D; :: thesis: ( x in X implies {x} common_on_dom H )
assume A2: x in X ; :: thesis: {x} common_on_dom H
thus {x} <> {} ; :: according to SEQFUNC:def 9 :: thesis: for n being Nat holds {x} c= dom (H . n)

now :: thesis: for n being Nat holds {x} c= dom (H . n)

let n be Nat; :: thesis: {x} c= dom (H . n)
X c= dom (H . n) by A1;
hence {x} c= dom (H . n) by A2, ZFMISC_1:31; :: thesis: verum

end;

hence for n being Nat holds {x} c= dom (H . n) ; :: thesis: verum