:: deftheorem Def2 defines ^ RFUNCT_1:def 2 :
for f being complex-valued Function
for b₂ being Function holds
( b₂ = f ^ iff ( dom b₂ = (dom f) \ (f " {0}) & ( for c being object st c in dom b₂ holds
b₂ . c = (f . c) " ) ) );