theorem Th28: :: MOD_2:28

for D, D9 being non empty set
for UN being Universe
for f being Function of D,D9 st D in UN & D9 in UN holds
f in UN