:: deftheorem defines . AOFA_I00:def 21 :
for X being non empty set
for i being Integer holds . (i,X) = (Funcs (X,INT)) --> i;