theorem Th20: :: CFUNCDOM:20

for x1, x2 being set
for A being non empty set
for f, g being Element of Funcs (A,COMPLEX) st A = {x1,x2} & x1 <> x2 & ( 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 ) ) ) holds
for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))