let X be non empty set ; :: thesis: for S being SigmaField of X
for f, g being PartFunc of X,REAL st dom f in S & dom g in S holds
dom (f + g) in S
let S be SigmaField of X; :: thesis: for f, g being PartFunc of X,REAL st dom f in S & dom g in S holds
dom (f + g) in S
let f, g be PartFunc of X,REAL; :: thesis: ( dom f in S & dom g in S implies dom (f + g) in S )
assume ( dom f in S & dom g in S ) ; :: thesis: dom (f + g) in S
then reconsider E1 = dom f, E2 = dom g as Element of S ;
dom (f + g) = E1 /\ E2 by VALUED_1:def 1;
hence dom (f + g) in S ; :: thesis: verum