let A be non empty set ; :: thesis: for x1 being Element of A ex f being Element of Funcs (A,REAL) st

( f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) )

let x1 be Element of A; :: thesis: ex f being Element of Funcs (A,REAL) st

( f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) )

deffunc H_{1}( object ) -> Element of REAL = In (0,REAL);

deffunc H_{2}( object ) -> Element of NAT = 1;

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

A1: for z being object st z in A holds

( ( S_{1}[z] implies H_{2}(z) in REAL ) & ( not S_{1}[z] implies H_{1}(z) in REAL ) )
by XREAL_0:def 1;

consider f being Function of A,REAL such that

A2: for z being object st z in A holds

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

reconsider f = f as Element of Funcs (A,REAL) by FUNCT_2:8;

take f ; :: thesis: ( f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) )

thus ( f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) ) by A2; :: thesis: verum

( f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) )

let x1 be Element of A; :: thesis: ex f being Element of Funcs (A,REAL) st

( f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) )

deffunc H

deffunc H

defpred S

A1: for z being object st z in A holds

( ( S

consider f being Function of A,REAL such that

A2: for z being object st z in A holds

( ( S

reconsider f = f as Element of Funcs (A,REAL) by FUNCT_2:8;

take f ; :: thesis: ( f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) )

thus ( f . x1 = 1 & ( for z being set st z in A & z <> x1 holds

f . z = 0 ) ) by A2; :: thesis: verum