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

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