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))

<%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1) = <%(- x),(1. L)%> . ((1 + 1) -' 1) by POLYNOM5:40
.= <%(- x),(1. L)%> . 1 by NAT_D:34
.= 1. L by POLYNOM5:38 ;
then A3: (<%(- 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) ;
p is non-zero by A2, Th14;
then A4: len (poly_quotient (p,x)) > 0 by A1, Th44;

now :: thesis: ( len p = len (<%(- x),(1. L)%> *' (poly_quotient (p,x))) & ( for k being Nat st k < len p holds
p . k = (<%(- x),(1. L)%> *' (poly_quotient (p,x))) . k ) )

len (<%(- x),(1. L)%> *' (poly_quotient (p,x))) = ((len <%(- x),(1. L)%>) + (len (poly_quotient (p,x)))) - 1 by A4, A3, Th15, POLYNOM4:10
.= ((len (poly_quotient (p,x))) + (1 + 1)) - 1 by POLYNOM5:40
.= (len (poly_quotient (p,x))) + 1
.= len p by A1, A2, Def6 ;
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
defpred S₁[ Nat] means p . $1 = (<%(- x),(1. L)%> *' (poly_quotient (p,x))) . $1;
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
A5: 0. L = eval (p,x) by A1
.= eval ((poly_shift (p,0)),x) by Th39
.= (x * (eval ((poly_shift (p,(0 + 1))),x))) + (p . 0) by A2, Th42 ;
A6: (- x) * (eval ((poly_shift (p,(0 + 1))),x)) = ((- x) * (eval ((poly_shift (p,(0 + 1))),x))) + (0. L) by RLVECT_1:def 4
.= (((- x) * (eval ((poly_shift (p,(0 + 1))),x))) + (x * (eval ((poly_shift (p,1)),x)))) + (p . 0) by A5, RLVECT_1:def 3
.= ((- (x * (eval ((poly_shift (p,(0 + 1))),x)))) + (x * (eval ((poly_shift (p,1)),x)))) + (p . 0) by VECTSP_1:9
.= (0. L) + (p . 0) by RLVECT_1:5
.= p . 0 by RLVECT_1:4 ;
A7: 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]
A8: (poly_quotient (p,x)) . (k + 1) = eval ((poly_shift (p,((k + 1) + 1))),x) by A1, A2, Def6;
A9: (poly_quotient (p,x)) . k = eval ((poly_shift (p,(k + 1))),x) by A1, A2, Def6;

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

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

then A11: (poly_quotient (p,x)) . (k + 1) = eval ((0_. L),x) by A8, Th40, NAT_1:12
.= 0. L by POLYNOM4:17 ;
A12: (poly_quotient (p,x)) . k = eval ((0_. L),x) by A9, A10, Th40
.= 0. L by POLYNOM4:17 ;
(<%(- x),(1. L)%> *' (poly_quotient (p,x))) . (k + 1) = ((- x) * ((poly_quotient (p,x)) . (k + 1))) + ((1. L) * ((poly_quotient (p,x)) . k)) by Th34
.= (0. L) + ((1. L) * ((poly_quotient (p,x)) . k)) by A11
.= (0. L) + (0. L) by A12
.= 0. L by RLVECT_1:4 ;
hence S₁[k + 1] by A10, ALGSEQ_1:8; :: 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 A9, Th42;
then A13: (- (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 3
.= (0. L) + (p . (k + 1)) by A8, RLVECT_1:5 ;
(<%(- x),(1. L)%> *' (poly_quotient (p,x))) . (k + 1) = ((- x) * ((poly_quotient (p,x)) . (k + 1))) + ((1. L) * ((poly_quotient (p,x)) . k)) by Th34
.= ((- x) * ((poly_quotient (p,x)) . (k + 1))) + ((poly_quotient (p,x)) . k)
.= (- (x * ((poly_quotient (p,x)) . (k + 1)))) + ((poly_quotient (p,x)) . k) by VECTSP_1:9 ;
hence S₁[k + 1] by A13, RLVECT_1:4; :: thesis: verum

end;

end;

end;

(<%(- x),(1. L)%> *' (poly_quotient (p,x))) . 0 = (- x) * ((poly_quotient (p,x)) . 0) by Th34
.= (- x) * (eval ((poly_shift (p,(0 + 1))),x)) by A1, A2, Def6 ;
then A14: S₁[ 0 ] by A6;
for k being Nat holds S₁[k] from NAT_1:sch 2(A14, A7);
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:12; :: 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, Def6, POLYNOM4:5;
hence p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by POLYNOM3:34; :: thesis: verum

end;

end;