let A be set ; :: thesis: the_unity_wrt (FinPairUnion A) = [({}. A),({}. A)]
[({}. A),({}. A)] is_a_unity_wrt FinPairUnion A by Th17;
hence the_unity_wrt (FinPairUnion A) = [({}. A),({}. A)] by BINOP_1:def 8; :: thesis: verum