let A be set ; :: thesis: the_unity_wrt (FinUnion A) is_a_unity_wrt FinUnion A
FinUnion A is having_a_unity by Th53;
hence the_unity_wrt (FinUnion A) is_a_unity_wrt FinUnion A by Th22; :: thesis: verum