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

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