theorem Th19: :: NORMFORM:19

for A being set holds the_unity_wrt (FinPairUnion A) = [({}. A),({}. A)]