theorem :: FOMODEL0:37

for x being set
for U being non empty set
for u being Element of U
for p being FinSequence st p is U * -valued holds
(x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) by Lm48;