:: deftheorem Def2 defines . FUNCT_1:def 2 :
for f being Function
for x being object
for b₃ being set holds
( ( x in dom f implies ( b₃ = f . x iff [x,b₃] in f ) ) & ( not x in dom f implies ( b₃ = f . x iff b₃ = {} ) ) );