:: deftheorem defines Funcs AIMLOOP:def 1 :
for X, Y being 1-sorted holds Funcs (X,Y) = Funcs ( the carrier of X, the carrier of Y);