let A be set ; :: thesis: FinUnion A is having_a_unity
{}. A is_a_unity_wrt FinUnion A by Th37;
hence FinUnion A is having_a_unity ; :: thesis: verum