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

per cases ( len F = 0 or len F = 1 or len F = 2 ) by A2, Th40, NAT_1:27;

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

then A4: <%z0,z1%> = 0_. L by A2, POLYNOM4:8;
hence eval <%z0,z1%>,x = 0. L by POLYNOM4:20
.= (0_. L) . 0 by FUNCOP_1:13
.= z0 by A4, Th39
.= z0 + (0. L) by RLVECT_1:def 7
.= z0 + ((0. L) * x) by VECTSP_1:39
.= z0 + (((0_. L) . 1) * x) by FUNCOP_1:13
.= z0 + (z1 * x) by A4, Th39 ;
:: thesis: verum

end;

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

then 0 + 1 in Seg (len F) by FINSEQ_1:6;
then 1 in dom F by FINSEQ_1:def 3;
then F . 1 = (<%z0,z1%> . (1 -' 1)) * ((power L) . x,(1 -' 1)) by A3
.= (<%z0,z1%> . 0 ) * ((power L) . x,(1 -' 1)) by XREAL_1:234
.= (<%z0,z1%> . 0 ) * ((power L) . x,0 ) by XREAL_1:234
.= z0 * ((power L) . x,0 ) by Th39
.= z0 * (1_ L) by GROUP_1:def 8
.= z0 by GROUP_1:def 5 ;
then F = <*z0*> by A5, FINSEQ_1:57;
hence eval <%z0,z1%>,x = z0 by A1, RLVECT_1:61
.= z0 + (0. L) by RLVECT_1:def 7
.= z0 + ((0. L) * x) by VECTSP_1:39
.= z0 + ((<%z0,z1%> . 1) * x) by A2, A5, ALGSEQ_1:22
.= z0 + (z1 * x) by Th39 ;
:: thesis: verum

end;

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

then 1 in dom F by FINSEQ_3:27;
then A7: F . 1 = (<%z0,z1%> . (1 -' 1)) * ((power L) . x,(1 -' 1)) by A3
.= (<%z0,z1%> . 0 ) * ((power L) . x,(1 -' 1)) by XREAL_1:234
.= (<%z0,z1%> . 0 ) * ((power L) . x,0 ) by XREAL_1:234
.= z0 * ((power L) . x,0 ) by Th39
.= z0 * (1_ L) by GROUP_1:def 8
.= z0 by GROUP_1:def 5 ;
A8: 2 -' 1 = 2 - 1 by XREAL_0:def 2;
2 in dom F by A6, FINSEQ_3:27;
then F . 2 = (<%z0,z1%> . (2 -' 1)) * ((power L) . x,(2 -' 1)) by A3
.= z1 * ((power L) . x,1) by A8, Th39
.= z1 * x by GROUP_1:98 ;
then F = <*z0,(z1 * x)*> by A6, A7, FINSEQ_1:61;
hence eval <%z0,z1%>,x = z0 + (z1 * x) by A1, RLVECT_1:62; :: thesis: verum

end;

end;