for K being Ring
for n, m being Nat holds
( len (0. (K,n,m)) = n & dom (0. (K,n,m)) = Seg n )