for C1, C2 being Category
for F being Functor of C1,C2 holds F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) is ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)))