defpred S₁[ Element of NAT , Real] means ( ( $1 = 0 implies $2 = 0 ) & ( $1 > 0 implies $2 = log (2,$1) ) );
A1: for x being Element of NAT ex y being Element of REAL st S₁[x,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of REAL st S₁[n,y]

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: ex y being Element of REAL st S₁[n,y]

hence ex y being Element of REAL st S₁[n,y] ; :: thesis: verum

end;

suppose n > 0 ; :: thesis: ex y being Element of REAL st S₁[n,y]

hence ex y being Element of REAL st S₁[n,y] ; :: thesis: verum

end;

end;

end;

consider h being Function of NAT,REAL such that
A2: for x being Element of NAT holds S₁[x,h . x] from FUNCT_2:sch 3(A1);
take h ; :: thesis: ( h . 0 = 0 & ( for n being Element of NAT st n > 0 holds
h . n = log (2,n) ) )
thus h . 0 = 0 by A2; :: thesis: for n being Element of NAT st n > 0 holds
h . n = log (2,n)
let n be Element of NAT ; :: thesis: ( n > 0 implies h . n = log (2,n) )
thus ( n > 0 implies h . n = log (2,n) ) by A2; :: thesis: verum