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 H1( object ) -> Element of REAL = In (0,REAL);
deffunc H2( object ) -> Element of NAT = 1;
defpred S1[ object ] means \$1 = x1;
A1: for z being object st z in A holds
( ( S1[z] implies H2(z) in REAL ) & ( not S1[z] implies H1(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
( ( S1[z] implies f . z = H2(z) ) & ( not S1[z] implies f . z = H1(z) ) ) from 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