for i being Element of I holds (I --> T) . i is T_0 TopSpace by FUNCOP_1:13;
hence product (I --> T) is T_0 by Th38; :: thesis: verum