theorem :: FOMODEL0:53

for Y being set
for U1, U2 being non empty set
for p being FinSequence st U1 c= U2 & Y c= U1 * & p is Y -valued & p <> {} & Y is with_non-empty_elements holds
(U1 -multiCat) . p = (U2 -multiCat) . p