:: deftheorem defines +~ FUNCT_4:def 5 :
for f being Function
for x, y being object holds f +~ (x,y) = f +* ((x .--> y) * f);