theorem Th20: :: FOMODEL0:20

for f being Function holds f = { [x,(f . x)] where x is Element of dom f : x in dom f }