defpred S₁[ object ] means $1 is polynomially-abs-bounded Function of NAT,REAL;
consider IT being set such that
A01: for x being object holds
( x in IT iff ( x in Funcs (NAT,REAL) & S₁[x] ) ) from XBOOLE_0:sch 1();
A1: for x being object holds
( x in IT iff x is polynomially-abs-bounded Function of NAT,REAL )

proof

let x be object ; :: thesis: ( x in IT iff x is polynomially-abs-bounded Function of NAT,REAL )
( x is polynomially-abs-bounded Function of NAT,REAL implies x in Funcs (NAT,REAL) ) by FUNCT_2:8;
hence ( x in IT iff x is polynomially-abs-bounded Function of NAT,REAL ) by A01; :: thesis: verum

end;

for x being object st x in IT holds
x in Funcs (NAT,REAL)

proof

let x be object ; :: thesis: ( x in IT implies x in Funcs (NAT,REAL) )
assume x in IT ; :: thesis: x in Funcs (NAT,REAL)
then x is polynomially-abs-bounded Function of NAT,REAL by A1;
hence x in Funcs (NAT,REAL) by FUNCT_2:8; :: thesis: verum

end;

then IT is Subset of (RAlgebra NAT) by TARSKI:def 3;
hence ex b₁ being Subset of (RAlgebra NAT) st
for x being object holds
( x in b₁ iff x is polynomially-abs-bounded Function of NAT,REAL ) by A1; :: thesis: verum