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 FUNCT_2:sch 5(A1);
 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 FUNCT_2:sch 5(A3);
 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