theorem Th7: :: HILB10_5:8

for n being Ordinal
for p being Polynomial of n,F_Real st |.p.| = 0_ (n,F_Real) holds
p = 0_ (n,F_Real)