:: deftheorem Def35 defines </> VALUED_2:def 35 :
for f being complex-functions-valued Function
for b2 being Function holds
( b2 = </> f iff ( dom b2 = dom f & ( for x being object st x in dom b2 holds
b2 . x = (f . x) " ) ) );