theorem Th20: :: FUNCT_6:24

for X being set
for f being Function holds
( doms (X --> f) = X --> (dom f) & rngs (X --> f) = X --> (rng f) )