let A be set ; :: thesis: FinPairUnion A is having_a_unity
[({}. A),({}. A)] is_a_unity_wrt FinPairUnion A by Th17;
hence FinPairUnion A is having_a_unity by SETWISEO:def 2; :: thesis: verum