theorem Th17: :: CLOSURE2:17

for i being set
for f being Function st i in dom f holds
|.{f}.| . i = {(f . i)}