for X being set
for L being List of X
for O being Operation of X
for n being Nat holds L WHEREle (O,n) = L WHERElt (O,(n + 1))