for x being set
for U, U1 being non empty set st (U -multiCat) . x is U1 -valued & x in (U *) * holds
x is FinSequence of U1 *