for x being object
for n, m being Nat holds m |-> (n |-> x) is tabular