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

[({}. A),({}. A)] is_a_unity_wrt FinPairUnion A by Th17;

hence FinPairUnion A is having_a_unity by SETWISEO:def 2; :: thesis: verum