(U -multiCat) . x in U * by Th40;
hence (U -multiCat) . x is U -valued ; :: thesis: verum