theorem :: VECTSP_1:36

for L being non empty right_complementable add-associative right_zeroed unital right-distributive doubleLoopStr
for n being Element of NAT st n > 0 holds
(power L) . ((0. L),n) = 0. L