let L be non empty unital doubleLoopStr ; :: thesis: for x being Element of L holds eval ((0_. L),x) = 0. L
let x be Element of L; :: thesis: eval ((0_. L),x) = 0. L
consider F being FinSequence of the carrier of L such that
A1: eval ((0_. L),x) = Sum F and
A2: len F = len (0_. L) and
for n being Element of NAT st n in dom F holds
F . n = ((0_. L) . (n -' 1)) * ((power L) . (x,(n -' 1))) by Def2;
len F = 0 by A2, Th3;
then F = <*> the carrier of L ;
hence eval ((0_. L),x) = 0. L by A1, RLVECT_1:43; :: thesis: verum