:: deftheorem defines extended_by AOFA_L00:def 3 :
for X being Function
for J, Y being set holds X extended_by (Y,J) = (J --> Y) +* (X | J);