:: deftheorem defines VAL ZF_MODEL:def 2 :
for D being non empty set holds VAL D = Funcs (VAR,D);