theorem :: FINSEQ_1:90

for x, y being object st x in dom <*y*> holds
x = 1