theorem Th17: :: CFUNCDOM:17

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