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 (BRoots p)
let p be non-zero Polynomial of L; :: thesis: ( p . ((len p) -' 1) = 1. L implies p = poly_with_roots (BRoots p) )
assume A1: p . ((len p) -' 1) = 1. L ; :: thesis: p = poly_with_roots (BRoots p)
defpred S₁[ 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 (BRoots p);
len p > 0 by Th14;
then A2: len p >= 0 + 1 by NAT_1:13;
A3: for n being Nat st n >= 1 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 1 & S₁[n] implies S₁[n + 1] )
assume that
A4: n >= 1 and
A5: S₁[n] ; :: thesis: S₁[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 (BRoots p) )
assume that
A6: len p = n + 1 and
n + 1 >= 1 and
A7: p . ((len p) -' 1) = 1. L ; :: thesis: p = poly_with_roots (BRoots p)
n + 1 > 1 by A4, NAT_1:13;
then p is with_roots by A6, POLYNOM5:def 9;
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 A8, Th47;
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 A11, VECTSP_2:def 1;
then A12: len p = ((len q) + (1 + 1)) - 1 by A9, A10, POLYNOM4:10;
q . ((len q) -' 1) = 1. L by A7, A9, Th38;
then A13: q = poly_with_roots (BRoots q) 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) + (BRoots q) by A9, Th53;
hence p = poly_with_roots (BRoots p) by A9, A13, A14, Th61; :: thesis: verum

end;

A15: S₁[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 (BRoots p) )
assume that
A16: len p = 1 and
1 >= 1 and
A17: p . ((len p) -' 1) = 1. L ; :: thesis: p = poly_with_roots (BRoots p)
degree (BRoots p) = 0 by A16, Th54;
then A18: BRoots p = EmptyBag the carrier of L by Th9;
(len p) -' 1 = 0 by A16, XREAL_1:232;
hence p = <%(1. L)%> by A16, A17, ALGSEQ_1:def 5
.= poly_with_roots (BRoots p) by A18, Th57 ;
:: thesis: verum

end;

for n being Nat st n >= 1 holds
S₁[n] from NAT_1:sch 8(A15, A3);
hence p = poly_with_roots (BRoots p) by A1, A2; :: thesis: verum