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