:: deftheorem Def2 defines +* FUNCT_7:def 3 :
for f being Function
for i, x being object holds
( ( i in dom f implies f +* (i,x) = f +* (i .--> x) ) & ( not i in dom f implies f +* (i,x) = f ) );