defpred S₁[ object ] means $1 is negligible 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 negligible Function of NAT,REAL )

proof

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

end;

for x being object st x in IT holds
x in Big_Oh_poly

proof

let x be object ; :: thesis: ( x in IT implies x in Big_Oh_poly )
assume x in IT ; :: thesis: x in Big_Oh_poly
then x is negligible Function of NAT,REAL by A1;
hence x in Big_Oh_poly by DefX1; :: thesis: verum

end;

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