let L be non empty right_complementable add-associative right_zeroed left-distributive unital 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;
len F <= 2 by A2, Th39;
then not not len F = 0 & ... & not len F = 2 ;

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

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

then A4: <%z0,z1%> = 0_. L by A2, POLYNOM4:5;
hence eval (<%z0,z1%>,x) = 0. L by POLYNOM4:17
.= (0_. L) . 0 by FUNCOP_1:7
.= z0 by A4, Th38
.= z0 + (0. L) by RLVECT_1:def 4
.= z0 + ((0. L) * x)
.= z0 + (((0_. L) . 1) * x) by FUNCOP_1:7
.= z0 + (z1 * x) by A4, Th38 ;
:: 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:4;
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:232
.= (<%z0,z1%> . 0) * ((power L) . (x,0)) by XREAL_1:232
.= z0 * ((power L) . (x,0)) by Th38
.= z0 * (1_ L) by GROUP_1:def 7
.= z0 by GROUP_1:def 4 ;
then F = <*z0*> by A5, FINSEQ_1:40;
hence eval (<%z0,z1%>,x) = z0 by A1, RLVECT_1:44
.= z0 + (0. L) by RLVECT_1:def 4
.= z0 + ((0. L) * x)
.= z0 + ((<%z0,z1%> . 1) * x) by A2, A5, ALGSEQ_1:8
.= z0 + (z1 * x) by Th38 ;
:: thesis: verum

end;

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

then 1 in dom F by FINSEQ_3:25;
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:232
.= (<%z0,z1%> . 0) * ((power L) . (x,0)) by XREAL_1:232
.= z0 * ((power L) . (x,0)) by Th38
.= z0 * (1_ L) by GROUP_1:def 7
.= z0 by GROUP_1:def 4 ;
A8: 2 -' 1 = 2 - 1 by XREAL_0:def 2;
2 in dom F by A6, FINSEQ_3:25;
then F . 2 = (<%z0,z1%> . (2 -' 1)) * ((power L) . (x,(2 -' 1))) by A3
.= z1 * ((power L) . (x,1)) by A8, Th38
.= z1 * x by GROUP_1:50 ;
then F = <*z0,(z1 * x)*> by A6, A7, FINSEQ_1:44;
hence eval (<%z0,z1%>,x) = z0 + (z1 * x) by A1, RLVECT_1:45; :: thesis: verum

end;

end;