let L be non degenerated comRing; :: thesis: for r being Element of L
for p being Polynomial of L st r is_a_root_of p holds
p = <%(- r),(1. L)%> *' (poly_quotient p,r)
let x be Element of L; :: thesis: for p being Polynomial of L st x is_a_root_of p holds
p = <%(- x),(1. L)%> *' (poly_quotient p,x)
let p be Polynomial of L; :: thesis: ( x is_a_root_of p implies p = <%(- x),(1. L)%> *' (poly_quotient p,x) )
assume A1: x is_a_root_of p ; :: thesis: p = <%(- x),(1. L)%> *' (poly_quotient p,x)
set r = <%(- x),(1. L)%>;
set pq = poly_quotient p,x;

per cases ( len p > 0 or len p = 0 ) ;

suppose A2: len p > 0 ; :: thesis: p = <%(- x),(1. L)%> *' (poly_quotient p,x)

then p is non-zero by Th19;
then A3: len (poly_quotient p,x) > 0 by A1, Th49;
<%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1) = <%(- x),(1. L)%> . ((1 + 1) -' 1) by POLYNOM5:41
.= <%(- x),(1. L)%> . 1 by NAT_D:34
.= 1. L by POLYNOM5:39 ;
then A4: (<%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1)) * ((poly_quotient p,x) . ((len (poly_quotient p,x)) -' 1)) = (poly_quotient p,x) . ((len (poly_quotient p,x)) -' 1) by VECTSP_1:def 19;

now

len (<%(- x),(1. L)%> *' (poly_quotient p,x)) = ((len <%(- x),(1. L)%>) + (len (poly_quotient p,x))) - 1 by A3, A4, Th20, POLYNOM4:13
.= ((len (poly_quotient p,x)) + (1 + 1)) - 1 by POLYNOM5:41
.= (len (poly_quotient p,x)) + 1
.= len p by A1, A2, Def7 ;
hence len p = len (<%(- x),(1. L)%> *' (poly_quotient p,x)) ; :: thesis: for k being Nat st k < len p holds
p . k = (<%(- x),(1. L)%> *' (poly_quotient p,x)) . k
let k be Nat; :: thesis: ( k < len p implies p . k = (<%(- x),(1. L)%> *' (poly_quotient p,x)) . k )
assume k < len p ; :: thesis: p . k = (<%(- x),(1. L)%> *' (poly_quotient p,x)) . k
defpred S₁[ Nat] means p . $1 = (<%(- x),(1. L)%> *' (poly_quotient p,x)) . $1;
A5: (<%(- x),(1. L)%> *' (poly_quotient p,x)) . 0 = (- x) * ((poly_quotient p,x) . 0 ) by Th39
.= (- x) * (eval (poly_shift p,(0 + 1)),x) by A1, A2, Def7 ;
A6: 0. L = eval p,x by A1, POLYNOM5:def 6
.= eval (poly_shift p,0 ),x by Th44
.= (x * (eval (poly_shift p,(0 + 1)),x)) + (p . 0 ) by A2, Th47 ;
(- x) * (eval (poly_shift p,(0 + 1)),x) = ((- x) * (eval (poly_shift p,(0 + 1)),x)) + (0. L) by RLVECT_1:def 7
.= (((- x) * (eval (poly_shift p,(0 + 1)),x)) + (x * (eval (poly_shift p,1),x))) + (p . 0 ) by A6, RLVECT_1:def 6
.= ((- (x * (eval (poly_shift p,(0 + 1)),x))) + (x * (eval (poly_shift p,1),x))) + (p . 0 ) by VECTSP_1:41
.= (0. L) + (p . 0 ) by RLVECT_1:16
.= p . 0 by RLVECT_1:10 ;
then A7: S₁[ 0 ] by A5;
A8: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
A9: (poly_quotient p,x) . (k + 1) = eval (poly_shift p,((k + 1) + 1)),x by A1, A2, Def7;
A10: (poly_quotient p,x) . k = eval (poly_shift p,(k + 1)),x by A1, A2, Def7;

per cases ( k + 1 >= len p or k + 1 < len p ) ;

suppose A11: k + 1 >= len p ; :: thesis: S₁[k + 1]

then A12: (poly_quotient p,x) . k = eval (0_. L),x by A10, Th45
.= 0. L by POLYNOM4:20 ;
A13: (poly_quotient p,x) . (k + 1) = eval (0_. L),x by A9, A11, Th45, NAT_1:12
.= 0. L by POLYNOM4:20 ;
(<%(- x),(1. L)%> *' (poly_quotient p,x)) . (k + 1) = ((- x) * ((poly_quotient p,x) . (k + 1))) + ((1. L) * ((poly_quotient p,x) . k)) by Th39
.= (0. L) + ((1. L) * ((poly_quotient p,x) . k)) by A13, VECTSP_1:36
.= (0. L) + (0. L) by A12, VECTSP_1:36
.= 0. L by RLVECT_1:10 ;
hence S₁[k + 1] by A11, ALGSEQ_1:22; :: thesis: verum

end;

suppose k + 1 < len p ; :: thesis: S₁[k + 1]

then (poly_quotient p,x) . k = (x * (eval (poly_shift p,((k + 1) + 1)),x)) + (p . (k + 1)) by A10, Th47;
then A14: (- (x * ((poly_quotient p,x) . (k + 1)))) + ((poly_quotient p,x) . k) = ((- (x * ((poly_quotient p,x) . (k + 1)))) + (x * (eval (poly_shift p,((k + 1) + 1)),x))) + (p . (k + 1)) by RLVECT_1:def 6
.= (0. L) + (p . (k + 1)) by A9, RLVECT_1:16 ;
(<%(- x),(1. L)%> *' (poly_quotient p,x)) . (k + 1) = ((- x) * ((poly_quotient p,x) . (k + 1))) + ((1. L) * ((poly_quotient p,x) . k)) by Th39
.= ((- x) * ((poly_quotient p,x) . (k + 1))) + ((poly_quotient p,x) . k) by VECTSP_1:def 19
.= (- (x * ((poly_quotient p,x) . (k + 1)))) + ((poly_quotient p,x) . k) by VECTSP_1:41 ;
hence S₁[k + 1] by A14, RLVECT_1:10; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A8);
hence p . k = (<%(- x),(1. L)%> *' (poly_quotient p,x)) . k ; :: thesis: verum

end;

hence p = <%(- x),(1. L)%> *' (poly_quotient p,x) by ALGSEQ_1:28; :: thesis: verum

end;

suppose len p = 0 ; :: thesis: p = <%(- x),(1. L)%> *' (poly_quotient p,x)

then ( poly_quotient p,x = 0_. L & p = 0_. L ) by A1, Def7, POLYNOM4:8;
hence p = <%(- x),(1. L)%> *' (poly_quotient p,x) by POLYNOM3:35; :: thesis: verum

end;

end;