:: deftheorem defines +* AOFA_000:def 4 :
for f, g being Function
for X being set holds (f,X) +* g = g +* (f | X);