theorem Th55: :: HILB10_7:55

for f being FinSequence holds doms <*f*> = { <*i*> where i is Element of NAT : i in dom f }