theorem Th20: :: NORMFORM:20

for A being set
for x being Element of [:(Fin A),(Fin A):] holds the_unity_wrt (FinPairUnion A) c= x