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