reconsider IB = I --> L as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I ;
for i being Element of I holds IB . i is complete LATTICE ;
hence ( product (I --> L) is with_suprema & product (I --> L) is complete ) by WAYBEL_3:31; :: thesis: verum