defpred S1[ Element of NAT , Real] means ( ( $1 = 0 implies $2 = 0 ) & ( $1 > 0 implies $2 = $1 to_power a ) );
A1: for x being Element of NAT ex y being Element of REAL st S1[x,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of REAL st S1[n,y]
per cases ( n = zz or n > 0 ) ;
suppose n = zz ; :: thesis: ex y being Element of REAL st S1[n,y]
hence ex y being Element of REAL st S1[n,y] ; :: thesis: verum
end;
suppose A2: n > 0 ; :: thesis: ex y being Element of REAL st S1[n,y]
n to_power a in REAL by XREAL_0:def 1;
hence ex y being Element of REAL st S1[n,y] by A2; :: thesis: verum
end;
end;
end;
consider h being sequence of REAL such that
A3: for x being Element of NAT holds S1[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 = n to_power a ) )
thus h . 0 = 0 by A3; :: thesis: for n being Element of NAT st n > 0 holds
h . n = n to_power a
let n be Element of NAT ; :: thesis: ( n > 0 implies h . n = n to_power a )
thus ( n > 0 implies h . n = n to_power a ) by A3; :: thesis: verum