theorem Th53: :: POLYNOM5:53
for L being Field
for p, q being Polynomial of L
for x being Element of L holds eval ((Subst (p,q)),x) = eval (p,(eval (q,x)))