theorem Th5: :: ENS_1:5

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 V