theorem Th17: :: NECKLA_3:17

for G1, G2 being RelStr st the carrier of G1 misses the carrier of G2 holds
ComplRelStr (union_of (G1,G2)) = sum_of ((ComplRelStr G1),(ComplRelStr G2))