let C, D be Category; :: thesis: Funct (C,D) c= bool [: the carrier' of C, the carrier' of D:]

now :: thesis: for x being object st x in Funct (C,D) holds
x in bool [: the carrier' of C, the carrier' of D:]

let x be object ; :: thesis: ( x in Funct (C,D) implies x in bool [: the carrier' of C, the carrier' of D:] )
assume x in Funct (C,D) ; :: thesis: x in bool [: the carrier' of C, the carrier' of D:]
then reconsider x9 = x as Function of the carrier' of C, the carrier' of D by CAT_2:def 2;
x9 c= [: the carrier' of C, the carrier' of D:] ;
hence x in bool [: the carrier' of C, the carrier' of D:] ; :: thesis: verum

end;

hence Funct (C,D) c= bool [: the carrier' of C, the carrier' of D:] ; :: thesis: verum