let V be non empty set ; :: thesis: for C being Category
for T being Function of the carrier' of C,(Maps (Hom C)) st Hom C c= V holds
T is Function of the carrier' of C, the carrier' of (Ens V)
let C be Category; :: thesis: for T being Function of the carrier' of C,(Maps (Hom C)) st Hom C c= V holds
T is Function of the carrier' of C, the carrier' of (Ens V)
let T be Function of the carrier' of C,(Maps (Hom C)); :: thesis: ( Hom C c= V implies T is Function of the carrier' of C, the carrier' of (Ens V) )
assume Hom C c= V ; :: thesis: T is Function of the carrier' of C, the carrier' of (Ens V)
then Maps (Hom C) c= Maps V by Th7;
hence T is Function of the carrier' of C, the carrier' of (Ens V) by FUNCT_2:7; :: thesis: verum