for K being Field
for f being FinSequence of NAT holds
( Len (1. (K,f)) = f & Width (1. (K,f)) = f )