let D be non empty set ; :: thesis: for Y being RealNormSpace
for H1, H2 being Functional_Sequence of D, the carrier of Y
for X being set st X common_on_dom H1 & X common_on_dom H2 holds
( X common_on_dom H1 + H2 & X common_on_dom H1 - H2 )
let Y be RealNormSpace; :: thesis: for H1, H2 being Functional_Sequence of D, the carrier of Y
for X being set st X common_on_dom H1 & X common_on_dom H2 holds
( X common_on_dom H1 + H2 & X common_on_dom H1 - H2 )
let H1, H2 be Functional_Sequence of D, the carrier of Y; :: thesis: for X being set st X common_on_dom H1 & X common_on_dom H2 holds
( X common_on_dom H1 + H2 & X common_on_dom H1 - H2 )
let X be set ; :: thesis: ( X common_on_dom H1 & X common_on_dom H2 implies ( X common_on_dom H1 + H2 & X common_on_dom H1 - H2 ) )
assume that
A1: X common_on_dom H1 and
A2: X common_on_dom H2 ; :: thesis: ( X common_on_dom H1 + H2 & X common_on_dom H1 - H2 )

now :: thesis: for n being Nat holds X c= dom ((H1 + H2) . n)

let n be Nat; :: thesis: X c= dom ((H1 + H2) . n)
( X c= dom (H1 . n) & X c= dom (H2 . n) ) by A1, A2;
then X c= (dom (H1 . n)) /\ (dom (H2 . n)) by XBOOLE_1:19;
then X c= dom ((H1 . n) + (H2 . n)) by VFUNCT_1:def 1;
hence X c= dom ((H1 + H2) . n) by Def5; :: thesis: verum

end;

hence X common_on_dom H1 + H2 by A1; :: thesis: X common_on_dom H1 - H2

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

let n be Nat; :: thesis: X c= dom ((H1 - H2) . n)
( X c= dom (H1 . n) & X c= dom (H2 . n) ) by A1, A2;
then X c= (dom (H1 . n)) /\ (dom (H2 . n)) by XBOOLE_1:19;
then X c= dom ((H1 . n) - (H2 . n)) by VFUNCT_1:def 2;
hence X c= dom ((H1 - H2) . n) by Th3; :: thesis: verum

end;

hence X common_on_dom H1 - H2 by A1; :: thesis: verum