let x1 be set ; for A being non empty set ex f, g being Element of Funcs A,REAL st
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( 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 = 1 ) ) ) )
let A be non empty set ; ex f, g being Element of Funcs A,REAL st
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( 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 = 1 ) ) ) )
deffunc H1( set ) -> Element of NAT = 1;
deffunc H2( set ) -> Element of NAT = 0 ;
defpred S1[ set ] means $1 = x1;
A1:
for z being set st z in A holds
( ( S1[z] implies H1(z) in REAL ) & ( not S1[z] implies H2(z) in REAL ) )
;
consider f being Function of A,REAL such that
A2:
for z being set 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 set st z in A holds
( ( S1[z] implies H2(z) in REAL ) & ( not S1[z] implies H1(z) in REAL ) )
;
consider g being Function of A,REAL such that
A4:
for z being set 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,REAL by FUNCT_2:11;
take
f
; ex g being Element of Funcs A,REAL st
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( 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 = 1 ) ) ) )
take
g
; ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( 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 = 1 ) ) ) )
thus
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( 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 = 1 ) ) ) )
by A2, A4; verum