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)
len p > 0 by Th19;
then A2: len p >= 0 + 1 by NAT_1:13;
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);
A3: 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
A4: len p = 1 and
1 >= 1 and
A5: p . ((len p) -' 1) = 1. L ; :: thesis: p = poly_with_roots (BRoots p)
degree (BRoots p) = 0 by A4, Th59;
then A6: BRoots p = EmptyBag the carrier of L by Th14;
(len p) -' 1 = 0 by A4, XREAL_1:234;
hence p = <%(1. L)%> by A4, A5, ALGSEQ_1:def 6
.= poly_with_roots (BRoots p) by A6, Th62 ;
:: thesis: verum

end;

A7: 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
A8: n >= 1 and
A9: 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
A10: len p = n + 1 and
n + 1 >= 1 and
A11: p . ((len p) -' 1) = 1. L ; :: thesis: p = poly_with_roots (BRoots p)
n + 1 > 1 by A8, NAT_1:13;
then p is with_roots by A10, POLYNOM5:def 8;
then consider x being Element of L such that
A12: x is_a_root_of p by POLYNOM5:def 7;
set q = poly_quotient p,x;
set r = <%(- x),(1. L)%>;
A13: p = <%(- x),(1. L)%> *' (poly_quotient p,x) by A12, Th52;
then reconsider q = poly_quotient p,x as non-zero Polynomial of L by Th36;
BRoots <%(- x),(1. L)%> = {x},1 -bag by Th56;
then A14: BRoots p = ({x},1 -bag ) + (BRoots q) by A13, Th58;
A15: len <%(- x),(1. L)%> = 2 by POLYNOM5:41;
len q > 0 by Th19;
then ( <%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1) <> 0. L & q . ((len q) -' 1) <> 0. L ) by A15, Th20;
then (<%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1)) * (q . ((len q) -' 1)) <> 0. L by VECTSP_2:def 5;
then A16: len p = ((len q) + (1 + 1)) - 1 by A13, A15, POLYNOM4:13;
q . ((len q) -' 1) = 1. L by A11, A13, Th43;
then A17: q = poly_with_roots (BRoots q) by A8, A9, A10, A16;
poly_with_roots ({x},1 -bag ) = <%(- x),(1. L)%> by Th63;
hence p = poly_with_roots (BRoots p) by A13, A14, A17, Th66; :: thesis: verum

end;

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