let A be set ; :: thesis: the_unity_wrt (FinUnion A) is_a_unity_wrt FinUnion A
thus the_unity_wrt (FinUnion A) is_a_unity_wrt FinUnion A by Th14, Th41; :: thesis: verum