defpred S₁[ Nat, object ] means $2 = (((- 1) |^ $1) * (r |^ ((2 * $1) + 1))) / ((2 * $1) + 1);
A1: for n being Element of NAT ex y being Element of REAL st S₁[n,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of REAL st S₁[n,y]
(((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1) in REAL by XREAL_0:def 1;
hence ex y being Element of REAL st S₁[n,y] ; :: thesis: verum

end;

consider f being Function of NAT,REAL such that
A2: for x being Element of NAT holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for n being Nat holds f . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1)
let i be Nat; :: thesis: f . i = (((- 1) |^ i) * (r |^ ((2 * i) + 1))) / ((2 * i) + 1)
i in NAT by ORDINAL1:def 12;
hence f . i = (((- 1) |^ i) * (r |^ ((2 * i) + 1))) / ((2 * i) + 1) by A2; :: thesis: verum