for p, q being FinSequence holds
( len p < len q iff dom p c< dom q )