for A being non empty set
for x1 being Element of A ex f being Element of Funcs (A,REAL) st
( f . x1 = 1 & ( for z being set st z in A & z <> x1 holds
f . z = 0 ) )