A1: T |^ S = product (S --> T) by YELLOW_1:def 5;
for i being Element of S holds (S --> T) . i is complete LATTICE ;
hence T |^ S is complete by A1, WAYBEL_3:31; :: thesis: verum