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

per cases ( len F = 0 or len F = 1 ) by A4, NAT_1:25;

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

then A5: <%z0%> = 0_. L by A2, POLYNOM4:5;
hence eval (<%z0%>,x) = 0. L by POLYNOM4:17
.= (0_. L) . 0 by FUNCOP_1:7
.= z0 by A5, Th32 ;
:: thesis: verum

end;

suppose A6: len F = 1 ; :: thesis: eval (<%z0%>,x) = z0

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%> . (1 -' 1)) * ((power L) . (x,(1 -' 1))) by A3
.= (<%z0%> . 0) * ((power L) . (x,(1 -' 1))) by XREAL_1:232
.= (<%z0%> . 0) * ((power L) . (x,0)) by XREAL_1:232
.= z0 * ((power L) . (x,0)) by Th32
.= z0 * (1_ L) by GROUP_1:def 7
.= z0 by GROUP_1:def 4 ;
then F = <*z0*> by A6, FINSEQ_1:40;
hence eval (<%z0%>,x) = z0 by A1, RLVECT_1:44; :: thesis: verum

end;

end;