set IB = I --> X;
for i being Element of I holds (I --> X) . i is lower-bounded algebraic LATTICE ;
hence product (I --> X) is algebraic by WAYBEL13:25; :: thesis: verum