theorem Th2: :: MATRIX_0:2

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