for x being set
for U1, U2 being non empty set
for p being FinSequence holds
( ( (U1 -multiCat) . x <> {} & (U2 -multiCat) . x <> {} implies (U1 -multiCat) . x = (U2 -multiCat) . x ) & ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {} * -valued ) )