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