let TM1, TM2 be second-countable finite-ind metrizable TopSpace; :: thesis: ( ind TM2 = 0 implies ind [:TM1,TM2:] = ind TM1 )
assume A1: ind TM2 = 0 ; :: thesis: ind [:TM1,TM2:] = ind TM1
then A2: not TM2 is empty by 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:31;
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 not TM1 is empty ; :: thesis: ind [:TM1,TM2:] = ind TM1
then ind [:(TM2 | X),TM1:] = ind TM1 by A2, BORSUK_3:13, TOPDIM_1:25;
then A5: ind [:TM1,(TM2 | X):] = ind TM1 by TOPDIM_1:28;
A6: [:TM1,(TM2 | X):] is SubSpace of [:TM1,TM2:] by BORSUK_3:15;
then [#] [:TM1,(TM2 | X):] c= [#] [:TM1,TM2:] by PRE_TOPC:def 4;
then reconsider cT12 = [#] [:TM1,(TM2 | X):] as Subset of [:TM1,TM2:] ;
[:TM1,(TM2 | X):] = [:TM1,TM2:] | cT12 by A6, PRE_TOPC:def 5;
then ind cT12 = ind TM1 by A5, 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;