let TM2, TM1 be metrizable second-countable finite-ind TopSpace; :: thesis: ( ind TM2 = 0 implies ind [:TM1,TM2:] = ind TM1 )
assume A1: ind TM2 = 0 ; :: thesis: ind [:TM1,TM2:] = ind TM1
A2: not TM2 is empty by A1, TOPDIM_1:6;
then A3: ind [:TM1,TM2:] <= (ind TM1) + 0 by A1, Lm5;
set x = the Point of TM2;
reconsider X = {the Point of TM2} as Subset of TM2 by A2, ZFMISC_1:37;

per cases ( TM1 is empty or not TM1 is empty ) ;

suppose A4: TM1 is empty ; :: thesis: ind [:TM1,TM2:] = ind TM1

then ind TM1 = - 1 by TOPDIM_1:6;
hence ind [:TM1,TM2:] = ind TM1 by A4, TOPDIM_1:6; :: thesis: verum

end;

suppose A5: not TM1 is empty ; :: thesis: ind [:TM1,TM2:] = ind TM1

ind [:(TM2 | X),TM1:] = ind TM1 by A5, A2, BORSUK_3:15, TOPDIM_1:25;
then A6: ind [:TM1,(TM2 | X):] = ind TM1 by TOPDIM_1:28;
A7: [:TM1,(TM2 | X):] is SubSpace of [:TM1,TM2:] by BORSUK_3:17;
then [#] [:TM1,(TM2 | X):] c= [#] [:TM1,TM2:] by PRE_TOPC:def 9;
then reconsider cT12 = [#] [:TM1,(TM2 | X):] as Subset of [:TM1,TM2:] ;
[:TM1,(TM2 | X):] = [:TM1,TM2:] | cT12 by A7, PRE_TOPC:def 10;
then ind cT12 = ind TM1 by A6, TOPDIM_1:17;
then ind TM1 <= ind [:TM1,TM2:] by TOPDIM_1:19;
hence ind [:TM1,TM2:] = ind TM1 by A3, XXREAL_0:1; :: thesis: verum

end;

end;