theorem Th4: :: NUMERAL2:4

for X, Y being finite natural-membered set st X misses Y holds
dom ((Sgm0 X) ^ (Sgm0 Y)) = dom (Sgm0 (X \/ Y))