theorem Th15: :: ENS_1:15

for V being non empty set
for A, B being Element of V
for f being Function of A,B st ( B = {} implies A = {} ) holds
[[A,B],f] in Maps (A,B)