let D be non empty set ; :: thesis: for H1, H2 being Functional_Sequence of D,REAL
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 & X common_on_dom H1 (#) H2 )
let H1, H2 be Functional_Sequence of D,REAL; :: 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 & 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 & 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 & X common_on_dom H1 (#) H2 )
A3: X <> {} by A1;
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 VALUED_1:def 1;
hence X c= dom ((H1 + H2) . n) by Def5; :: thesis: verum
end;
hence X common_on_dom H1 + H2 by A3; :: 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 VALUED_1:12;
hence X c= dom ((H1 - H2) . n) by Th3; :: thesis: verum
end;
hence X common_on_dom H1 - H2 by A3; :: 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 VALUED_1:def 4;
hence X c= dom ((H1 (#) H2) . n) by Def7; :: thesis: verum
end;
hence X common_on_dom H1 (#) H2 by A3; :: thesis: verum