for n being Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for x being Function of n,L holds eval ((0_ (n,L)),x) = 0. L