:: deftheorem Def3 defines UnivF MODELC_1:def 3 :
for f being Function
for x, a being set holds
( ( x in dom f implies UnivF (x,f,a) = f . x ) & ( not x in dom f implies UnivF (x,f,a) = a ) );