let L be non empty right_complementable Abelian add-associative right_zeroed left-distributive well-unital unital associative doubleLoopStr ; :: thesis: for p being Polynomial of L
for x being Element of L ex d being Element of L st eval (p,x) = (d * x) + (p . 0)
let p be Polynomial of L; :: thesis: for x being Element of L ex d being Element of L st eval (p,x) = (d * x) + (p . 0)
let x be Element of L; :: thesis: ex d being Element of L st eval (p,x) = (d * x) + (p . 0)
consider F being FinSequence of the carrier of L such that
A1: ( eval (p,x) = Sum F & len F = len p ) and
A2: for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) by POLYNOM4:def 2;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len p implies ex d being Element of L st Sum (F | $1) = (d * x) + (p . 0) );
A3: S₁[ 0 ] ;
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
assume A6: ( 1 <= i + 1 & i + 1 <= len p ) ; :: thesis: ex d being Element of L st Sum (F | (i + 1)) = (d * x) + (p . 0)
reconsider I = i as Element of NAT by ORDINAL1:def 12;
set i1 = I + 1;
I + 1 in dom F by A6, A1, FINSEQ_3:25;
then A7: F | (I + 1) = (F | i) ^ <*(F . (I + 1))*> by FINSEQ_5:10;
A8: F . (I + 1) = (p . ((I + 1) -' 1)) * ((power L) . (x,((I + 1) -' 1))) by A6, A1, FINSEQ_3:25, A2;
then A9: Sum (F | (I + 1)) = (Sum (F | i)) + ((p . ((I + 1) -' 1)) * ((power L) . (x,((I + 1) -' 1)))) by A7, FVSUM_1:71;

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

suppose A10: i = 0 ; :: thesis: ex d being Element of L st Sum (F | (i + 1)) = (d * x) + (p . 0)

then len (F | i) = 0 ;
then Sum (F | i) = 0. L by RLVECT_1:75;
then Sum (F | (I + 1)) = (p . 0) * (1_ L) by A9, A10, GROUP_1:def 7
.= ((0. L) * x) + (p . 0) ;
hence ex d being Element of L st Sum (F | (i + 1)) = (d * x) + (p . 0) ; :: thesis: verum

end;

suppose A11: i > 0 ; :: thesis: ex d being Element of L st Sum (F | (i + 1)) = (d * x) + (p . 0)

then consider d being Element of L such that
A12: Sum (F | i) = (d * x) + (p . 0) by A5, A6, NAT_1:13, NAT_1:14;
reconsider e = I - 1 as Element of NAT by A11, NAT_1:20;
e + 1 = I ;
then A13: (power L) . (x,I) = ((power L) . (x,e)) * x by GROUP_1:def 7;
Sum (F | (I + 1)) = ((d * x) + (p . 0)) + ((p . I) * ((power L) . (x,I))) by A12, A8, A7, FVSUM_1:71
.= (p . 0) + ((d * x) + ((p . I) * ((power L) . (x,I)))) by RLVECT_1:def 3
.= (p . 0) + ((d * x) + (((p . I) * ((power L) . (x,e))) * x)) by A13, GROUP_1:def 3
.= (p . 0) + ((d + ((p . I) * ((power L) . (x,e)))) * x) by VECTSP_1:def 3 ;
hence ex d being Element of L st Sum (F | (i + 1)) = (d * x) + (p . 0) ; :: thesis: verum

end;

end;

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
then A14: S₁[ len p] ;

per cases ( len p = 0 or 1 <= len p ) by NAT_1:14;

suppose len p = 0 ; :: thesis: ex d being Element of L st eval (p,x) = (d * x) + (p . 0)

then p = 0_. L by POLYNOM4:5;
then eval (p,x) = ((0. L) * x) + (p . 0) by POLYNOM4:17;
hence ex d being Element of L st eval (p,x) = (d * x) + (p . 0) ; :: thesis: verum

end;

suppose 1 <= len p ; :: thesis: ex d being Element of L st eval (p,x) = (d * x) + (p . 0)

hence ex d being Element of L st eval (p,x) = (d * x) + (p . 0) by A1, A14; :: thesis: verum

end;

end;