theorem Th6: :: POLYNOM9:6
for n being Nat
for x being Element of F_Real st x <> 0. F_Real holds
(power F_Real) . (x,n) <> 0. F_Real