defpred S₁[ Nat] means for T1, T2 being TopSpace st T1,T2 are_homeomorphic & T1 is finite-ind & ind T1 <= $1 holds
( T2 is finite-ind & ind T2 <= ind T1 );
let T1, T2 be TopSpace; :: thesis:
assume that
A1: T1,T2 are_homeomorphic and
A2: T1 is finite-ind ; :: thesis:
reconsider i = (ind T1) + 1 as Nat by A2, Lm3;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A4: S₁[n] ; :: thesis:
set n1 = n + 1;
let T1, T2 be TopSpace; :: thesis:
assume that
A5: T1,T2 are_homeomorphic and
A6: T1 is finite-ind and
A7: ind T1 <= n + 1 ; :: thesis:
consider f being Function of T1,T2 such that
A8: f is being_homeomorphism by A5, T_0TOPSP:def 1;
set f9 = f " ;
A9: dom f = [#] T1 by A8;
A10: rng f = [#] T2 by A8;
A11: f is onto by A10;
A12: f is one-to-one by A8;

suppose A13: [#] T1 = {} T1 ; :: thesis:

then ind T1 = - 1 by Th6;
hence ( T2 is finite-ind & ind T2 <= ind T1 ) by A10, A13, Th6; :: thesis:

end;

suppose A14: [#] T1 <> {} T1 ; :: thesis:

then not T1 is empty ;
then reconsider i = ind T1 as Nat by A6, TARSKI:1;
A15: not T1 is empty by A14;
A16: not T2 is empty by A9, A14;

per cases by A7, NAT_1:8;

suppose i <= n ; :: thesis:

hence ( T2 is finite-ind & ind T2 <= ind T1 ) by A4, A5, A6; :: thesis:

end;

suppose A17: ind T1 = n + 1 ; :: thesis:

A18: dom (f ") = [#] T2 by A10, A12, A16, TOPS_2:49;
A19: for p being Point of T2
for U being open Subset of T2 st p in U holds
ex W being open Subset of T2 st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (n + 1) - 1 )

reconsider F = f as Function ;
let p be Point of T2; :: thesis:
let U be open Subset of T2; :: thesis:
assume p in U ; :: thesis:
then A20: (f ") . p in (f ") .: U by A18, FUNCT_1:def 6;
( f " U = (f ") .: U & f " U is open ) by A8, A15, A16, TOPGRP_1:26, TOPS_2:55;
then consider W being open Subset of T1 such that
A21: (f ") . p in W and
A22: W c= f " U and
A23: Fr W is finite-ind and
A24: ind (Fr W) <= (n + 1) - 1 by A6, A17, A20, Th16;
set FW = Fr W;
A25: ind (T1 | (Fr W)) = ind (Fr W) by A23, Lm5;
Fr W,f .: (Fr W) are_homeomorphic by A8, METRIZTS:3;
then A26: T1 | (Fr W),T2 | (f .: (Fr W)) are_homeomorphic by METRIZTS:def 1;
then T2 | (f .: (Fr W)) is finite-ind by A4, A23, A24, A25;
then A27: f .: (Fr W) is finite-ind by Th18;
F " = f " by A11, A12, TOPS_2:def 4;
then A28: f . ((f ") . p) = p by A10, A12, A16, FUNCT_1:35;
ind (T2 | (f .: (Fr W))) <= ind (T1 | (Fr W)) by A4, A23, A24, A25, A26;
then A29: ind (T2 | (f .: (Fr W))) <= (n + 1) - 1 by A24, A25, XXREAL_0:2;
reconsider W9 = f .: W as open Subset of T2 by A8, A15, A16, TOPGRP_1:25;
take W9 ; :: thesis:
W9 c= f .: (f " U) by A22, RELAT_1:123;
hence ( p in W9 & W9 c= U ) by A9, A10, A21, A28, FUNCT_1:77, FUNCT_1:def 6; :: thesis:
f .: (Fr W) = f .: ((Cl W) \ W) by TOPS_1:42
.= (f .: (Cl W)) \ W9 by A12, FUNCT_1:64
.= (Cl W9) \ W9 by A8, A16, TOPS_2:60
.= Fr W9 by TOPS_1:42 ;
hence ( Fr W9 is finite-ind & ind (Fr W9) <= (n + 1) - 1 ) by A27, A29, Lm5; :: thesis:

end;

then T2 is finite-ind by Th15;
hence ( T2 is finite-ind & ind T2 <= ind T1 ) by A17, A19, Th16; :: thesis:

end;

end;

end;

end;

end;

let T1, T2 be TopSpace; :: thesis:
assume that
A31: T1,T2 are_homeomorphic and
A32: T1 is finite-ind and
A33: ind T1 <= 0 ; :: thesis:
consider f being Function of T1,T2 such that
A34: f is being_homeomorphism by A31, T_0TOPSP:def 1;
set f9 = f " ;
A35: dom f = [#] T1 by A34;
A36: rng f = [#] T2 by A34;
A37: f is onto by A36;
A38: f is one-to-one by A34;

suppose A39: [#] T1 = {} T1 ; :: thesis:

then ind T1 = - 1 by Th6;
hence ( T2 is finite-ind & ind T2 <= ind T1 ) by A36, A39, Th6; :: thesis:

end;

suppose A40: [#] T1 <> {} T1 ; :: thesis:

then not T1 is empty ;
then reconsider i = ind T1 as Nat by A32, TARSKI:1;
A41: i = 0 by A33;
A42: not T1 is empty by A40;
A43: not T2 is empty by A35, A40;
then A44: dom (f ") = [#] T2 by A36, A38, TOPS_2:49;
A45: for p being Point of T2
for U being open Subset of T2 st p in U holds
ex W being open Subset of T2 st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 0 - 1 )

reconsider F = f as Function ;
let p be Point of T2; :: thesis:
let U be open Subset of T2; :: thesis:
assume p in U ; :: thesis:
then A46: (f ") . p in (f ") .: U by A44, FUNCT_1:def 6;
F " = f " by A37, A38, TOPS_2:def 4;
then A47: f . ((f ") . p) = p by A36, A38, A43, FUNCT_1:35;
( f " U = (f ") .: U & f " U is open ) by A34, A42, A43, TOPGRP_1:26, TOPS_2:55;
then consider W being open Subset of T1 such that
A48: (f ") . p in W and
A49: W c= f " U and
A50: Fr W is finite-ind and
A51: ind (Fr W) <= 0 - 1 by A32, A33, A46, Th16;
reconsider W9 = f .: W as open Subset of T2 by A34, A42, A43, TOPGRP_1:25;
take W9 ; :: thesis:
W9 c= f .: (f " U) by A49, RELAT_1:123;
hence ( p in W9 & W9 c= U ) by A35, A36, A47, A48, FUNCT_1:77, FUNCT_1:def 6; :: thesis:
ind (Fr W) >= - 1 by A50, Th5;
then ind (Fr W) = - 1 by A51, XXREAL_0:1;
then Fr W = {} T1 by A50, Th6;
then W is closed by TOPGEN_1:14;
then W9 is closed by A34, A43, TOPS_2:58;
then Fr W9 = {} T2 by TOPGEN_1:14;
hence ( Fr W9 is finite-ind & ind (Fr W9) <= 0 - 1 ) by Th6; :: thesis:

end;

then T2 is finite-ind by Th15;
hence ( T2 is finite-ind & ind T2 <= ind T1 ) by A41, A45, Th16; :: thesis:

end;

end;

end;

A52: for n being Nat holds S₁[n] from NAT_1:sch 2(A30, A3);
(ind T1) + 0 <= i by XREAL_1:6;
hence ( T2 is finite-ind & ind T2 <= ind T1 ) by A1, A2, A52; :: thesis: