let f be ManySortedSet of X; :: thesis: ( f is d.union-distributive implies f is U-continuous )
dom f = X by PARTFUN1:def 4;
hence ( f is d.union-distributive implies f is U-continuous ) by Def14; :: thesis: verum