a in the Sorts of A . (the_sort_of a) by A, SORT;
then (f . (the_sort_of a)) . a is Element of the Sorts of B . (the_sort_of a) by FUNCT_2:5;
hence (f . (the_sort_of a)) . a is Element of B ; :: thesis: verum