theorem Th33: :: POLYNOM9:33

for x being object
for O being Ordinal
for R being non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p being Polynomial of O,R
for t, s being bag of O holds (Subst (t,x,p)) . (Subst (t,x,s)) = (p `^ (t . x)) . s by Def3;