theorem Th5: :: NUMERAL2:5

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