let a, b, x be Real; :: thesis: for n being Element of NAT st a <> 0 & not n is even & Polynom (a,b,0,(x |^ n)) = 0 & not x = 0 holds
x = n -root (- (b / a))
let n be Element of NAT ; :: thesis: ( a <> 0 & not n is even & Polynom (a,b,0,(x |^ n)) = 0 & not x = 0 implies x = n -root (- (b / a)) )
assume that
A1: a <> 0 and
A2: not n is even and
A3: Polynom (a,b,0,(x |^ n)) = 0 ; :: thesis: ( x = 0 or x = n -root (- (b / a)) )

now

per cases ( x |^ n = 0 or x |^ n = - (b / a) ) by A1, A3, Th5;

suppose x |^ n = 0 ; :: thesis: ( x = 0 or x = n -root (- (b / a)) )

hence ( x = 0 or x = n -root (- (b / a)) ) by PREPOWER:5; :: thesis: verum

end;

suppose x |^ n = - (b / a) ; :: thesis: ( x = 0 or x = n -root (- (b / a)) )

hence ( x = 0 or x = n -root (- (b / a)) ) by A2, POWER:4; :: thesis: verum

end;

end;

end;

hence ( x = 0 or x = n -root (- (b / a)) ) ; :: thesis: verum