let T1, T2 be TopSpace; :: thesis: for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic & A1 is finite-ind holds
ind A1 = ind A2
let A1 be Subset of T1; :: thesis: for A2 being Subset of T2 st A1,A2 are_homeomorphic & A1 is finite-ind holds
ind A1 = ind A2
let A2 be Subset of T2; :: thesis: ( A1,A2 are_homeomorphic & A1 is finite-ind implies ind A1 = ind A2 )
assume that
A1: A1,A2 are_homeomorphic and
A2: A1 is finite-ind ; :: thesis: ind A1 = ind A2
T1 | A1,T2 | A2 are_homeomorphic by A1, METRIZTS:def 1;
then A3: ind (T1 | A1) = ind (T2 | A2) by A2, Lm9;
( A2 is finite-ind & ind (T1 | A1) = ind A1 ) by A1, A2, Lm5, Th26;
hence ind A1 = ind A2 by A3, Lm5; :: thesis: verum