for x, y being set
for p being FinSequence of x st y in dom p holds
p . y in x