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

[({}. 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