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, Th6;
then F = <*> the carrier of L ;
hence eval (0_. L),x = 0. L by A1, RLVECT_1:60; :: thesis: verum