theorem Th1: :: ENS_1:1

for V being non empty set
for f being set holds
( f in Funcs V iff ex A, B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B ) )