defpred S₁[ Element of NAT , object ] means $2 = (p . ($1 + 1)) * ($1 + 1);
A1: for x being Element of NAT ex y being Element of F_Real st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of F_Real st S₁[x,y]
(p . (x + 1)) * (x + 1) is Element of F_Real by XREAL_0:def 1;
hence ex y being Element of F_Real st S₁[x,y] ; :: thesis: verum

end;

consider f being Function of NAT,F_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 = (p . (n + 1)) * (n + 1)
let n be Nat; :: thesis: f . n = (p . (n + 1)) * (n + 1)
n in NAT by ORDINAL1:def 12;
hence f . n = (p . (n + 1)) * (n + 1) by A2; :: thesis: verum