for n being Nat
for a being object holds len (n |-> a) = n