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

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