let L be non empty non degenerated right_complementable add-associative right_zeroed well-unital associative doubleLoopStr ; :: thesis: for x being Element of L holds eval ((1_. L),x) = 1. L
let x be Element of L; :: thesis: eval ((1_. L),x) = 1. L
consider F being FinSequence of the carrier of L such that
A1: eval ((1_. L),x) = Sum F and
A2: len F = len (1_. L) and
A3: for n being Element of NAT st n in dom F holds
F . n = ((1_. L) . (n -' 1)) * ((power L) . (x,(n -' 1))) by Def2;
A4: len F = 1 by A2, Th4;
then 1 in Seg (len F) by FINSEQ_1:1;
then 1 in dom F by FINSEQ_1:def 3;
then F . 1 = ((1_. L) . (1 -' 1)) * ((power L) . (x,(1 -' 1))) by A3
.= ((1_. L) . 0) * ((power L) . (x,(1 -' 1))) by XREAL_1:232
.= (1. L) * ((power L) . (x,(1 -' 1))) by POLYNOM3:30
.= (power L) . (x,(1 -' 1))
.= (power L) . (x,0) by XREAL_1:232
.= 1_ L by GROUP_1:def 7
.= 1. L ;
then F = <*(1. L)*> by A4, FINSEQ_1:40;
hence eval ((1_. L),x) = 1. L by A1, RLVECT_1:44; :: thesis: verum