theorem :: FUNCOP_1:46

for A being set
for X being non empty set
for x being Element of X holds A --> x is Function of A,X ;