theorem :: FUNCT_6:41

for X being set
for f being Function st X <> {} holds
( dom <:(X --> f):> = dom f & ( for x being object st x in dom f holds
<:(X --> f):> . x = X --> (f . x) ) )