let A be set ; :: thesis: the_unity_wrt (FinUnion A) = {}
{}. A is_a_unity_wrt FinUnion A by Th37;
hence the_unity_wrt (FinUnion A) = {} by BINOP_1:def 8; :: thesis: verum