let X be non empty set ; :: thesis: for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX 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,COMPLEX st dom f in S & dom g in S holds
dom (f + g) in S
let f, g be PartFunc of X,COMPLEX; :: thesis: ( dom f in S & dom g in S implies dom (f + g) in S )
assume that
A1: dom f in S and
A2: dom g in S ; :: thesis: dom (f + g) in S
reconsider E1 = dom f, E2 = dom g as Element of S by A1, A2;
dom (f + g) = E1 /\ E2 by VALUED_1:def 1;
hence dom (f + g) in S ; :: thesis: verum