theorem Th12: :: FUNCT_4:12

for f, g being Function
for x being object holds
( x in dom (f +* g) iff ( x in dom f or x in dom g ) )