theorem Th52: :: POLYNOM5:52

for L being Field
for p, q being Polynomial of L st len p <> 0 & len q > 1 holds
len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2