theorem :: TOPDIM_2:16

for TM1, TM2 being second-countable finite-ind metrizable TopSpace st ind TM2 = 0 holds
ind [:TM1,TM2:] = ind TM1