theorem Th15: :: CLOSURE2:15

for f being Function holds dom |.{f}.| = dom f