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 H_{1}( object ) -> Element of COMPLEX = 1r ;

deffunc H_{2}( object ) -> Element of COMPLEX = 0c ;

defpred S_{1}[ object ] means $1 = x1;

A1: for z being object st z in A holds

( ( S_{1}[z] implies H_{1}(z) in COMPLEX ) & ( not S_{1}[z] implies H_{2}(z) in COMPLEX ) )
;

consider f being Function of A,COMPLEX such that

A2: for z being object st z in A holds

( ( S_{1}[z] implies f . z = H_{1}(z) ) & ( not S_{1}[z] implies f . z = H_{2}(z) ) )
from FUNCT_2:sch 5(A1);

A3: for z being object st z in A holds

( ( S_{1}[z] implies H_{2}(z) in COMPLEX ) & ( not S_{1}[z] implies H_{1}(z) in COMPLEX ) )
;

consider g being Function of A,COMPLEX such that

A4: for z being object st z in A holds

( ( S_{1}[z] implies g . z = H_{2}(z) ) & ( not S_{1}[z] implies g . z = H_{1}(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

( ( 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 H

deffunc H

defpred S

A1: for z being object st z in A holds

( ( S

consider f being Function of A,COMPLEX such that

A2: for z being object st z in A holds

( ( S

A3: for z being object st z in A holds

( ( S

consider g being Function of A,COMPLEX such that

A4: for z being object st z in A holds

( ( S

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