let X be set ; :: thesis: for Y being complex-functions-membered set

for f being PartFunc of X,Y

for g being complex-valued Function holds dom (f <-> g) = (dom f) /\ (dom g)

let Y be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y

for g being complex-valued Function holds dom (f <-> g) = (dom f) /\ (dom g)

let f be PartFunc of X,Y; :: thesis: for g being complex-valued Function holds dom (f <-> g) = (dom f) /\ (dom g)

let g be complex-valued Function; :: thesis: dom (f <-> g) = (dom f) /\ (dom g)

thus dom (f <-> g) = (dom f) /\ (dom (- g)) by Def41

.= (dom f) /\ (dom g) by VALUED_1:8 ; :: thesis: verum

for f being PartFunc of X,Y

for g being complex-valued Function holds dom (f <-> g) = (dom f) /\ (dom g)

let Y be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y

for g being complex-valued Function holds dom (f <-> g) = (dom f) /\ (dom g)

let f be PartFunc of X,Y; :: thesis: for g being complex-valued Function holds dom (f <-> g) = (dom f) /\ (dom g)

let g be complex-valued Function; :: thesis: dom (f <-> g) = (dom f) /\ (dom g)

thus dom (f <-> g) = (dom f) /\ (dom (- g)) by Def41

.= (dom f) /\ (dom g) by VALUED_1:8 ; :: thesis: verum