:: deftheorem defines ^ AOFA_I00:def 20 :
for X being non empty set
for x being Element of X holds ^ x = (Funcs (X,INT)) --> x;