:: deftheorem defines Funcs ENS_1:def 1 :
for V being non empty set holds Funcs V = union { (Funcs (A,B)) where A, B is Element of V : verum } ;