defpred S₁[ object ] means $1 is Functor of C,D;
consider F being set such that
A1: for x being object holds
( x in F iff ( x in Funcs ( the carrier' of C, the carrier' of D) & S₁[x] ) ) from XBOOLE_0:sch 1();
take F ; :: thesis: for x being set holds
( x in F iff x is Functor of C,D )
let x be set ; :: thesis: ( x in F iff x is Functor of C,D )
thus ( x in F implies x is Functor of C,D ) by A1; :: thesis: ( x is Functor of C,D implies x in F )
assume A2: x is Functor of C,D ; :: thesis: x in F
then x in Funcs ( the carrier' of C, the carrier' of D) by FUNCT_2:8;
hence x in F by A1, A2; :: thesis: verum