:: deftheorem defines Maps ENS_1:def 7 :
for V being non empty set
for A, B being Element of V holds Maps (A,B) = { [[A,B],f] where f is Element of Funcs V : [[A,B],f] in Maps V } ;