:: deftheorem defines ReassignIn FOMODEL2:def 5 :
for f being Function
for x, y being set holds (x,y) ReassignIn f = f +* (x .--> ({} .--> y));