let L be non empty non degenerated right_complementable add-associative right_zeroed associative well-unital 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, Th7;
then 1 in Seg (len F) by FINSEQ_1:3;
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:234
.= (1. L) * ((power L) . x,(1 -' 1)) by POLYNOM3:31
.= (power L) . x,(1 -' 1) by VECTSP_1:def 19
.= (power L) . x,0 by XREAL_1:234
.= 1_ L by GROUP_1:def 8
.= 1. L ;
then F = <*(1. L)*> by A4, FINSEQ_1:57;
hence eval (1_. L),x = 1. L by A1, RLVECT_1:61; :: thesis: verum