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
( X common_on_dom ||.H.|| & 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
( X common_on_dom ||.H.|| & 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
( X common_on_dom ||.H.|| & X common_on_dom - H )
let X be set ; :: thesis: ( X common_on_dom H implies ( X common_on_dom ||.H.|| & X common_on_dom - H ) )
assume A1: X common_on_dom H ; :: thesis: ( X common_on_dom ||.H.|| & X common_on_dom - H )

now :: thesis: for n being Nat holds X c= dom (||.H.|| . n)

let n be Nat; :: thesis: X c= dom (||.H.|| . n)
dom (H . n) = dom ||.(H . n).|| by NORMSP_0:def 3
.= dom (||.H.|| . n) by Def4 ;
hence X c= dom (||.H.|| . n) by A1; :: thesis: verum

end;

hence X common_on_dom ||.H.|| by A1; :: thesis: X common_on_dom - H

now :: thesis: for n being Nat holds X c= dom ((- H) . n)

let n be Nat; :: thesis: X c= dom ((- H) . n)
dom (H . n) = dom (- (H . n)) by VFUNCT_1:def 5
.= dom ((- H) . n) by Def3 ;
hence X c= dom ((- H) . n) by A1; :: thesis: verum

end;

hence X common_on_dom - H by A1; :: thesis: verum