defpred S_{1}[ 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_{1}[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

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

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