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
( X common_on_dom abs H & 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
( X common_on_dom abs H & X common_on_dom - H )
let X be set ; :: thesis: ( X common_on_dom H implies ( X common_on_dom abs H & X common_on_dom - H ) )
assume A1: X common_on_dom H ; :: thesis: ( X common_on_dom abs H & X common_on_dom - H )
then A2: X <> {} by Def10;

now

let n be Element of NAT ; :: thesis: X c= dom ((abs H) . n)
dom (H . n) = dom (abs (H . n)) by VALUED_1:def 11
.= dom ((abs H) . n) by Def5 ;
hence X c= dom ((abs H) . n) by A1, Def10; :: thesis: verum

end;

hence X common_on_dom abs H by A2, Def10; :: thesis: X common_on_dom - H

now

let n be Element of NAT ; :: thesis: X c= dom ((- H) . n)
dom (H . n) = dom (- (H . n)) by VALUED_1:8
.= dom ((- H) . n) by Def4 ;
hence X c= dom ((- H) . n) by A1, Def10; :: thesis: verum

end;

hence X common_on_dom - H by A2, Def10; :: thesis: verum