defpred S₁[ set ] means $1 is Function;
ex Y being set st
for x being set holds
( x in Y iff ( x in X & S₁[x] ) ) from XBOOLE_0:sch 1();
hence ex b₁ being set st
for x being set holds
( x in b₁ iff ( x in X & x is Function ) ) ; :: thesis: verum