:: deftheorem Def13 defines functional FUNCT_1:def 13 :
for IT being set holds
( IT is functional iff for x being object st x in IT holds
x is Function );