theorem Th38: :: POLYDIFF:38

for n being Nat
for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for x, y being Element of L holds eval ((seq (n,x)),y) = ((seq (n,x)) . n) * (power (y,n))