per cases ( the carrier of T is empty or not the carrier of T is empty ) ;

suppose A1: the carrier of T is empty ; :: thesis: the adj-map of T . t is Subset of the adjectives of T

then dom the adj-map of T = the carrier of T ;
then the adj-map of T . t = {} the adjectives of T by A1, FUNCT_1:def 2;
hence the adj-map of T . t is Subset of the adjectives of T ; :: thesis: verum

end;

suppose not the carrier of T is empty ; :: thesis: the adj-map of T . t is Subset of the adjectives of T

then the adj-map of T . t in Fin the adjectives of T by FUNCT_2:5;
hence the adj-map of T . t is Subset of the adjectives of T by FINSUB_1:16; :: thesis: verum

end;

end;