theorem Th17: :: NORMFORM:17

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