:: deftheorem Def12 defines empty-preserving ROUGHS_2:def 12 :
for f being Function holds
( f is empty-preserving iff f . {} = {} );