let L be algebraic-closed domRing; :: thesis: for p being non-zero Polynomial of L st p . ((len p) -' 1) = 1. L holds
p = poly_with_roots ()

let p be non-zero Polynomial of L; :: thesis: ( p . ((len p) -' 1) = 1. L implies p = poly_with_roots () )
assume A1: p . ((len p) -' 1) = 1. L ; :: thesis:
defpred S1[ Nat] means for p being non-zero Polynomial of L st len p = \$1 & \$1 >= 1 & p . ((len p) -' 1) = 1. L holds
p = poly_with_roots ();
len p > 0 by Th14;
then A2: len p >= 0 + 1 by NAT_1:13;
A3: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
A4: n >= 1 and
A5: S1[n] ; :: thesis: S1[n + 1]
let p be non-zero Polynomial of L; :: thesis: ( len p = n + 1 & n + 1 >= 1 & p . ((len p) -' 1) = 1. L implies p = poly_with_roots () )
assume that
A6: len p = n + 1 and
n + 1 >= 1 and
A7: p . ((len p) -' 1) = 1. L ; :: thesis:
n + 1 > 1 by ;
then p is with_roots by ;
then consider x being Element of L such that
A8: x is_a_root_of p ;
set r = <%(- x),(1. L)%>;
set q = poly_quotient (p,x);
A9: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by ;
then reconsider q = poly_quotient (p,x) as non-zero Polynomial of L by Th31;
A10: len <%(- x),(1. L)%> = 2 by POLYNOM5:40;
then A11: <%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1) <> 0. L by Th15;
len q > 0 by Th14;
then q . ((len q) -' 1) <> 0. L by Th15;
then (<%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1)) * (q . ((len q) -' 1)) <> 0. L by ;
then A12: len p = ((len q) + (1 + 1)) - 1 by ;
q . ((len q) -' 1) = 1. L by A7, A9, Th38;
then A13: q = poly_with_roots () by A4, A5, A6, A12;
A14: poly_with_roots (({x},1) -bag) = <%(- x),(1. L)%> by Th58;
BRoots <%(- x),(1. L)%> = ({x},1) -bag by Th51;
then BRoots p = (({x},1) -bag) + () by ;
hence p = poly_with_roots () by A9, A13, A14, Th61; :: thesis: verum
end;
A15: S1[1]
proof
let p be non-zero Polynomial of L; :: thesis: ( len p = 1 & 1 >= 1 & p . ((len p) -' 1) = 1. L implies p = poly_with_roots () )
assume that
A16: len p = 1 and
1 >= 1 and
A17: p . ((len p) -' 1) = 1. L ; :: thesis:
degree () = 0 by ;
then A18: BRoots p = EmptyBag the carrier of L by Th9;
(len p) -' 1 = 0 by ;
hence p = <%(1. L)%> by
.= poly_with_roots () by ;
:: thesis: verum
end;
for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch 8(A15, A3);
hence p = poly_with_roots () by A1, A2; :: thesis: verum