for i being Element of I holds (I --> L) . i is transitive by FUNCOP_1:7;
hence product (I --> L) is transitive by WAYBEL_3:29; :: thesis: verum