let D be non empty set ; :: thesis: for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st X common_on_dom H holds
for x being set st x in X holds
{x} common_on_dom H
let Y be RealNormSpace; :: thesis: for H being Functional_Sequence of D, the carrier of Y
for X being set st X common_on_dom H holds
for x being set st x in X holds
{x} common_on_dom H
let H be Functional_Sequence of D, the carrier of Y; :: thesis: for X being set st X common_on_dom H holds
for x being set st x in X holds
{x} common_on_dom H
let X be set ; :: thesis: ( X common_on_dom H implies for x being set st x in X holds
{x} common_on_dom H )
assume A1: X common_on_dom H ; :: thesis: for x being set st x in X holds
{x} common_on_dom H
let x be set ; :: 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 b₁ being set holds {x} c= dom (H . b₁)

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 b₁ being set holds {x} c= dom (H . b₁) ; :: thesis: verum