for A being set holds FinPairUnion A is having_a_unity