for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for f being FinSequence of L
for i, j being Element of NAT st i in dom f & j = i - 1 holds
Ins ((Del (f,i)),j,(f /. i)) = f