let L be non empty non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive unital associative commutative domRing-like doubleLoopStr ; :: thesis: for p being Polynomial of L st p . 0 <> 0. L holds
ex q being Polynomial of L st
( len p = len q & q . 0 = 1. L & ( for i being Element of NAT st 0 < i holds
q . i = (p . i) * ((power L) . ((p . 0),(i -' 1))) ) & ( for x being Element of L holds eval (p,((p . 0) * x)) = (p . 0) * (eval (q,x)) ) )
let p be Polynomial of L; :: thesis: ( p . 0 <> 0. L implies ex q being Polynomial of L st
( len p = len q & q . 0 = 1. L & ( for i being Element of NAT st 0 < i holds
q . i = (p . i) * ((power L) . ((p . 0),(i -' 1))) ) & ( for x being Element of L holds eval (p,((p . 0) * x)) = (p . 0) * (eval (q,x)) ) ) )
assume A1: p . 0 <> 0. L ; :: thesis: ex q being Polynomial of L st
( len p = len q & q . 0 = 1. L & ( for i being Element of NAT st 0 < i holds
q . i = (p . i) * ((power L) . ((p . 0),(i -' 1))) ) & ( for x being Element of L holds eval (p,((p . 0) * x)) = (p . 0) * (eval (q,x)) ) )
defpred S₁[ Element of NAT , object ] means ( ( $1 = 0 implies $2 = 1. L ) & ( $1 > 0 implies $2 = (p . $1) * ((power L) . ((p . 0),($1 -' 1))) ) );
A2: for x being Element of NAT ex y being Element of L st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of L st S₁[x,y]

per cases ( x = 0 or x > 0 ) ;

suppose A3: x = 0 ; :: thesis: ex y being Element of L st S₁[x,y]

take 1. L ; :: thesis: S₁[x, 1. L]
thus S₁[x, 1. L] by A3; :: thesis: verum

end;

suppose A4: x > 0 ; :: thesis: ex y being Element of L st S₁[x,y]

take (p . x) * ((power L) . ((p . 0),(x -' 1))) ; :: thesis: S₁[x,(p . x) * ((power L) . ((p . 0),(x -' 1)))]
thus S₁[x,(p . x) * ((power L) . ((p . 0),(x -' 1)))] by A4; :: thesis: verum

end;

end;

end;

consider q being sequence of L such that
A5: for n being Element of NAT holds S₁[n,q . n] from FUNCT_2:sch 3(A2);

now :: thesis: for n being Nat st n >= (len p) + 1 holds
q . n = 0. L

let n be Nat; :: thesis: ( n >= (len p) + 1 implies q . n = 0. L )
assume A6: n >= (len p) + 1 ; :: thesis: q . n = 0. L
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A7: len p is_at_least_length_of p by ALGSEQ_1:def 3;
n > len p by A6, NAT_1:13;
then A8: p . nn = 0. L by A7, ALGSEQ_1:def 2;
q . nn = (p . nn) * ((power L) . ((p . 0),(nn -' 1))) by A5, A6;
hence q . n = 0. L by A8; :: thesis: verum

end;

then reconsider q = q as Polynomial of L by ALGSEQ_1:def 1;
take q ; :: thesis: ( len p = len q & q . 0 = 1. L & ( for i being Element of NAT st 0 < i holds
q . i = (p . i) * ((power L) . ((p . 0),(i -' 1))) ) & ( for x being Element of L holds eval (p,((p . 0) * x)) = (p . 0) * (eval (q,x)) ) )

A9: now :: thesis: for i being Nat st i >= len p holds
q . i = 0. L

let i be Nat; :: thesis: ( i >= len p implies q . i = 0. L )
assume A10: i >= len p ; :: thesis: q . i = 0. L
reconsider I = i as Element of NAT by ORDINAL1:def 12;
A11: len p is_at_least_length_of p by ALGSEQ_1:def 3;
then A12: p . i = 0. L by A10, ALGSEQ_1:def 2;
i > 0 by A11, A10, ALGSEQ_1:def 2, A1;
hence q . i = (p . I) * ((power L) . ((p . 0),(I -' 1))) by A5
.= 0. L by A12 ;
:: thesis: verum

end;

for m being Nat st m is_at_least_length_of q holds
len p <= m

proof

let m be Nat; :: thesis: ( m is_at_least_length_of q implies len p <= m )
assume A13: ( m is_at_least_length_of q & len p > m ) ; :: thesis: contradiction
reconsider lp = (len p) - 1 as Nat by A13;
q . m = 0. L by A13, ALGSEQ_1:def 2;
then A14: m <> 0 by A5;
for i being Nat st i >= m holds
p . i = 0. L

proof

let i be Nat; :: thesis: ( i >= m implies p . i = 0. L )
assume A15: ( i >= m & p . i <> 0. L ) ; :: thesis: contradiction
reconsider I = i as Element of NAT by ORDINAL1:def 12;
i > 0 by A15, A14;
then q . i = (p . I) * ((power L) . ((p . 0),(I -' 1))) by A5;
then (power L) . ((p . 0),(I -' 1)) = 0. L by A15, A13, ALGSEQ_1:def 2, VECTSP_2:def 1;
hence contradiction by A1, Th68; :: thesis: verum

end;

then m is_at_least_length_of p by ALGSEQ_1:def 2;
hence contradiction by A13, ALGSEQ_1:def 3; :: thesis: verum

end;

hence A16: ( len p = len q & q . 0 = 1. L ) by A9, A5, ALGSEQ_1:def 2, ALGSEQ_1:def 3; :: thesis: ( ( for i being Element of NAT st 0 < i holds
q . i = (p . i) * ((power L) . ((p . 0),(i -' 1))) ) & ( for x being Element of L holds eval (p,((p . 0) * x)) = (p . 0) * (eval (q,x)) ) )
thus for i being Element of NAT st 0 < i holds
q . i = (p . i) * ((power L) . ((p . 0),(i -' 1))) by A5; :: thesis: for x being Element of L holds eval (p,((p . 0) * x)) = (p . 0) * (eval (q,x))
let x be Element of L; :: thesis: eval (p,((p . 0) * x)) = (p . 0) * (eval (q,x))
consider P being FinSequence of the carrier of L such that
A17: ( eval (p,((p . 0) * x)) = Sum P & len P = len p ) and
A18: for n being Element of NAT st n in dom P holds
P . n = (p . (n -' 1)) * ((power L) . (((p . 0) * x),(n -' 1))) by POLYNOM4:def 2;
consider Q being FinSequence of the carrier of L such that
A19: ( eval (q,x) = Sum Q & len Q = len q ) and
A20: for n being Element of NAT st n in dom Q holds
Q . n = (q . (n -' 1)) * ((power L) . (x,(n -' 1))) by POLYNOM4:def 2;
reconsider Q = Q as Element of (len q) -tuples_on the carrier of L by A19, FINSEQ_2:92;
len P = len ((p . 0) * Q) by A17, A16, CARD_1:def 7;
then A21: dom P = dom ((p . 0) * Q) by FINSEQ_3:29;
for k being Nat st k in dom P holds
P . k = ((p . 0) * Q) . k

proof

let k be Nat; :: thesis: ( k in dom P implies P . k = ((p . 0) * Q) . k )
assume A22: k in dom P ; :: thesis: P . k = ((p . 0) * Q) . k
reconsider K = k as Element of NAT by ORDINAL1:def 12;
set k1 = K -' 1;
dom P = dom Q by A16, A17, A19, FINSEQ_3:29;
then Q . K = (q . (K -' 1)) * ((power L) . (x,(K -' 1))) by A22, A20;
then A23: ((p . 0) * Q) . K = (p . 0) * ((q . (K -' 1)) * ((power L) . (x,(K -' 1)))) by A21, A22, FVSUM_1:50;

per cases ( K -' 1 > 0 or K -' 1 = 0 ) ;

suppose A24: K -' 1 > 0 ; :: thesis: P . k = ((p . 0) * Q) . k

then K -' 1 >= 1 + 0 by NAT_1:8;
then (K -' 1) -' 1 = (K -' 1) - 1 by XREAL_1:233;
then ((K -' 1) -' 1) + 1 = K -' 1 ;
then A25: (p . 0) * ((power L) . ((p . 0),((K -' 1) -' 1))) = (power L) . ((p . 0),(K -' 1)) by GROUP_1:def 7;
((p . 0) * Q) . K = (p . 0) * (((p . (K -' 1)) * ((power L) . ((p . 0),((K -' 1) -' 1)))) * ((power L) . (x,(K -' 1)))) by A5, A24, A23
.= (p . 0) * ((p . (K -' 1)) * (((power L) . ((p . 0),((K -' 1) -' 1))) * ((power L) . (x,(K -' 1))))) by GROUP_1:def 3
.= (p . (K -' 1)) * ((p . 0) * (((power L) . ((p . 0),((K -' 1) -' 1))) * ((power L) . (x,(K -' 1))))) by GROUP_1:def 3
.= (p . (K -' 1)) * (((p . 0) * ((power L) . ((p . 0),((K -' 1) -' 1)))) * ((power L) . (x,(K -' 1)))) by GROUP_1:def 3
.= (p . (K -' 1)) * ((power L) . (((p . 0) * x),(K -' 1))) by GROUP_1:52, A25 ;
hence P . k = ((p . 0) * Q) . k by A22, A18; :: thesis: verum

end;

suppose A26: K -' 1 = 0 ; :: thesis: P . k = ((p . 0) * Q) . k

then ((p . 0) * Q) . K = (p . 0) * ((1. L) * ((power L) . (x,(K -' 1)))) by A5, A23
.= (p . (K -' 1)) * (1_ L) by A26, GROUP_1:def 7
.= (p . (K -' 1)) * ((power L) . (((p . 0) * x),(K -' 1))) by A26, GROUP_1:def 7 ;
hence P . k = ((p . 0) * Q) . k by A22, A18; :: thesis: verum

end;

end;

end;

then P = (p . 0) * Q by A21, FINSEQ_1:13;
hence eval (p,((p . 0) * x)) = (p . 0) * (eval (q,x)) by A17, A19, FVSUM_1:73; :: thesis: verum