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