for A being set holds the_unity_wrt (FinUnion A) is_a_unity_wrt FinUnion A by Th11, Th38;