theorem :: HILB10_5:9

for n being Ordinal
for p being Polynomial of n,F_Real holds degree p = degree |.p.|