let x1 be set ; :: thesis: 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 ) ) ) )

let A be non empty set ; :: thesis: 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 ) ) ) )

deffunc H1( object ) -> Element of COMPLEX = 1r ;
deffunc H2( object ) -> Element of COMPLEX = 0c ;
defpred S1[ object ] means \$1 = x1;
A1: for z being object st z in A holds
( ( S1[z] implies H1(z) in COMPLEX ) & ( not S1[z] implies H2(z) in COMPLEX ) ) ;
consider f being Function of A,COMPLEX such that
A2: for z being object st z in A holds
( ( S1[z] implies f . z = H1(z) ) & ( not S1[z] implies f . z = H2(z) ) ) from A3: for z being object st z in A holds
( ( S1[z] implies H2(z) in COMPLEX ) & ( not S1[z] implies H1(z) in COMPLEX ) ) ;
consider g being Function of A,COMPLEX such that
A4: for z being object st z in A holds
( ( S1[z] implies g . z = H2(z) ) & ( not S1[z] implies g . z = H1(z) ) ) from reconsider f = f, g = g as Element of Funcs (A,COMPLEX) by FUNCT_2:8;
take f ; :: thesis: ex 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 ) ) ) )

take g ; :: thesis: ( ( 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 ) ) ) )

thus ( ( 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 ) ) ) ) by A2, A4; :: thesis: verum