let L be non empty right_complementable add-associative right_zeroed left-distributive unital associative doubleLoopStr ; :: thesis: for z0, z1, z2, x being Element of L holds eval (<%z0,z1,z2%>,x) = (z0 + (z1 * x)) + ((z2 * x) * x)
let z0, z1, z2, x be Element of L; :: thesis: eval (<%z0,z1,z2%>,x) = (z0 + (z1 * x)) + ((z2 * x) * x)
consider F being FinSequence of L such that
A1: eval (<%z0,z1,z2%>,x) = Sum F and
A2: len F = len <%z0,z1,z2%> and
A3: for n being Element of NAT st n in dom F holds
F . n = (<%z0,z1,z2%> . (n -' 1)) * ((power L) . (x,(n -' 1))) by POLYNOM4:def 2;

A4: now :: thesis: ( 1 in dom F implies F . 1 = z0 )

assume 1 in dom F ; :: thesis: F . 1 = z0
hence F . 1 = (<%z0,z1,z2%> . (1 -' 1)) * ((power L) . (x,(1 -' 1))) by A3
.= (<%z0,z1,z2%> . 0) * ((power L) . (x,(1 -' 1))) by XREAL_1:232
.= (<%z0,z1,z2%> . 0) * ((power L) . (x,0)) by XREAL_1:232
.= z0 * ((power L) . (x,0)) by Th21
.= z0 * (1_ L) by GROUP_1:def 7
.= z0 by GROUP_1:def 4 ;
:: thesis: verum

end;

A5: now :: thesis: ( 2 in dom F implies F . 2 = z1 * x )

assume 2 in dom F ; :: thesis: F . 2 = z1 * x
hence F . 2 = (<%z0,z1,z2%> . (2 -' 1)) * ((power L) . (x,(2 -' 1))) by A3
.= z1 * ((power L) . (x,1)) by Lm1, Th22
.= z1 * x by GROUP_1:50 ;
:: thesis: verum

end;

not not len F = 0 & ... & not len F = 3 by A2, Th25;

per cases then ( len F = 0 or len F = 1 or len F = 2 or len F = 3 ) ;

suppose len F = 0 ; :: thesis: eval (<%z0,z1,z2%>,x) = (z0 + (z1 * x)) + ((z2 * x) * x)

then A6: <%z0,z1,z2%> = 0_. L by A2, POLYNOM4:5;
hence eval (<%z0,z1,z2%>,x) = 0. L by POLYNOM4:17
.= (0_. L) . 0 by FUNCOP_1:7
.= (z0 + (0. L)) + (0. L) by A6, Th21
.= (z0 + (((0_. L) . 1) * x)) + (((0. L) * x) * x) by FUNCOP_1:7
.= (z0 + (((0_. L) . 1) * x)) + ((((0_. L) . 2) * x) * x) by FUNCOP_1:7
.= (z0 + (z1 * x)) + ((((0_. L) . 2) * x) * x) by A6, Th22
.= (z0 + (z1 * x)) + ((z2 * x) * x) by A6, Th23 ;
:: thesis: verum

end;

suppose A7: len F = 1 ; :: thesis: eval (<%z0,z1,z2%>,x) = (z0 + (z1 * x)) + ((z2 * x) * x)

then 0 + 1 in Seg (len F) by FINSEQ_1:1;
then F = <*z0*> by A4, A7, FINSEQ_1:def 3, FINSEQ_1:40;
hence eval (<%z0,z1,z2%>,x) = z0 by A1, RLVECT_1:44
.= (z0 + ((0. L) * x)) + (((<%z0,z1,z2%> . 2) * x) * x) by A2, A7, ALGSEQ_1:8
.= (z0 + ((<%z0,z1,z2%> . 1) * x)) + (((<%z0,z1,z2%> . 2) * x) * x) by A2, A7, ALGSEQ_1:8
.= (z0 + (z1 * x)) + (((<%z0,z1,z2%> . 2) * x) * x) by Th22
.= (z0 + (z1 * x)) + ((z2 * x) * x) by Th23 ;
:: thesis: verum

end;

suppose A8: len F = 2 ; :: thesis: eval (<%z0,z1,z2%>,x) = (z0 + (z1 * x)) + ((z2 * x) * x)

F = <*z0,(z1 * x)*> by A4, A5, A8, FINSEQ_1:44, FINSEQ_3:25;
hence eval (<%z0,z1,z2%>,x) = (z0 + (z1 * x)) + (((0. L) * x) * x) by A1, RLVECT_1:45
.= (z0 + (z1 * x)) + (((<%z0,z1,z2%> . 2) * x) * x) by A2, A8, ALGSEQ_1:8
.= (z0 + (z1 * x)) + ((z2 * x) * x) by Th23 ;
:: thesis: verum

end;

suppose A9: len F = 3 ; :: thesis: eval (<%z0,z1,z2%>,x) = (z0 + (z1 * x)) + ((z2 * x) * x)

F . 3 = (<%z0,z1,z2%> . (3 -' 1)) * ((power L) . (x,(3 -' 1))) by A3, A9, FINSEQ_3:25
.= z2 * ((power L) . (x,2)) by Lm2, Th23
.= z2 * (x * x) by GROUP_1:51
.= (z2 * x) * x by GROUP_1:def 3 ;
then F = <*z0,(z1 * x),((z2 * x) * x)*> by A4, A5, A9, FINSEQ_1:45, FINSEQ_3:25;
hence eval (<%z0,z1,z2%>,x) = (z0 + (z1 * x)) + ((z2 * x) * x) by A1, RLVECT_1:46; :: thesis: verum

end;

end;