let T1, T2 be TopSpace; :: thesis: ( T1,T2 are_homeomorphic implies ( ( T1 is with_finite_small_inductive_dimension implies T2 is with_finite_small_inductive_dimension ) & ( T2 is with_finite_small_inductive_dimension implies T1 is with_finite_small_inductive_dimension ) & ( T1 is with_finite_small_inductive_dimension implies ind T2 = ind T1 ) ) )
assume A1: T1,T2 are_homeomorphic ; :: thesis: ( ( T1 is with_finite_small_inductive_dimension implies T2 is with_finite_small_inductive_dimension ) & ( T2 is with_finite_small_inductive_dimension implies T1 is with_finite_small_inductive_dimension ) & ( T1 is with_finite_small_inductive_dimension implies ind T2 = ind T1 ) )
consider f being Function of T1,T2 such that
A2: f is being_homeomorphism by A1, T_0TOPSP:def 1;
A3: dom f = [#] T1 by A2, TOPS_2:def 5;
A4: rng f = [#] T2 by A2, TOPS_2:def 5;

per cases ( [#] T1 = {} T1 or not T1 is empty ) ;

suppose A5: [#] T1 = {} T1 ; :: thesis: ( ( T1 is with_finite_small_inductive_dimension implies T2 is with_finite_small_inductive_dimension ) & ( T2 is with_finite_small_inductive_dimension implies T1 is with_finite_small_inductive_dimension ) & ( T1 is with_finite_small_inductive_dimension implies ind T2 = ind T1 ) )

then ind ([#] T2) = - 1 by A4, Th6;
hence ( ( T1 is with_finite_small_inductive_dimension implies T2 is with_finite_small_inductive_dimension ) & ( T2 is with_finite_small_inductive_dimension implies T1 is with_finite_small_inductive_dimension ) & ( T1 is with_finite_small_inductive_dimension implies ind T2 = ind T1 ) ) by A4, A5, Def4, Th6; :: thesis: verum

end;

suppose not T1 is empty ; :: thesis: ( ( T1 is with_finite_small_inductive_dimension implies T2 is with_finite_small_inductive_dimension ) & ( T2 is with_finite_small_inductive_dimension implies T1 is with_finite_small_inductive_dimension ) & ( T1 is with_finite_small_inductive_dimension implies ind T2 = ind T1 ) )

then reconsider t1 = T1, t2 = T2 as non empty TopSpace by A3;
A6: t2,t1 are_homeomorphic by A1;
hence ( T1 is with_finite_small_inductive_dimension iff T2 is with_finite_small_inductive_dimension ) by Lm8; :: thesis: ( T1 is with_finite_small_inductive_dimension implies ind T2 = ind T1 )
assume A7: T1 is with_finite_small_inductive_dimension ; :: thesis: ind T2 = ind T1
then T2 is with_finite_small_inductive_dimension by A1, Lm8;
then A8: ind T1 <= ind T2 by A6, Lm8;
ind T2 <= ind T1 by A1, A7, Lm8;
hence ind T2 = ind T1 by A8, XXREAL_0:1; :: thesis: verum

end;

end;