let TM1, TM2 be second-countable finite-ind metrizable TopSpace; :: thesis: ( ( not TM1 is empty or not TM2 is empty ) implies ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) )

defpred S_{1}[ Nat] means for TM1, TM2 being second-countable finite-ind metrizable TopSpace st ( not TM1 is empty or not TM2 is empty ) & ((ind TM1) + (ind TM2)) + 2 <= $1 holds

( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) );

reconsider i1 = (ind TM1) + 1, i2 = (ind TM2) + 1 as Nat by Lm1;

A1: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A40, A1);

((ind TM1) + (ind TM2)) + 2 = i1 + i2 ;

hence ( ( not TM1 is empty or not TM2 is empty ) implies ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) ) by A43; :: thesis: verum

defpred S

( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) );

reconsider i1 = (ind TM1) + 1, i2 = (ind TM2) + 1 as Nat by Lm1;

A1: for n being Nat st S

S

proof

A40:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let TM1, TM2 be second-countable finite-ind metrizable TopSpace; :: thesis: ( ( not TM1 is empty or not TM2 is empty ) & ((ind TM1) + (ind TM2)) + 2 <= n + 1 implies ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) )

assume that

A3: ( not TM1 is empty or not TM2 is empty ) and

A4: ((ind TM1) + (ind TM2)) + 2 <= n + 1 ; :: thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )

set T12 = [:TM1,TM2:];

end;assume A2: S

let TM1, TM2 be second-countable finite-ind metrizable TopSpace; :: thesis: ( ( not TM1 is empty or not TM2 is empty ) & ((ind TM1) + (ind TM2)) + 2 <= n + 1 implies ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) )

assume that

A3: ( not TM1 is empty or not TM2 is empty ) and

A4: ((ind TM1) + (ind TM2)) + 2 <= n + 1 ; :: thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )

set T12 = [:TM1,TM2:];

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

end;

suppose A5:
TM1 is empty
; :: thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )

then
ind TM1 = - 1
by TOPDIM_1:6;

then 0 + (- 1) <= (ind TM2) + (ind TM1) by A3, XREAL_1:6;

hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A5, TOPDIM_1:6; :: thesis: verum

end;then 0 + (- 1) <= (ind TM2) + (ind TM1) by A3, XREAL_1:6;

hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A5, TOPDIM_1:6; :: thesis: verum

suppose A6:
TM2 is empty
; :: thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )

then
ind TM2 = - 1
by TOPDIM_1:6;

then 0 + (- 1) <= (ind TM1) + (ind TM2) by A3, XREAL_1:6;

hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A6, TOPDIM_1:6; :: thesis: verum

end;then 0 + (- 1) <= (ind TM1) + (ind TM2) by A3, XREAL_1:6;

hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A6, TOPDIM_1:6; :: thesis: verum

suppose A7:
( not TM1 is empty & not TM2 is empty )
; :: thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )

then reconsider i1 = ind TM1, i2 = ind TM2 as Nat by TARSKI:1;

A8: for p being Point of [:TM1,TM2:]

for U being open Subset of [:TM1,TM2:] st p in U holds

ex W being open Subset of [:TM1,TM2:] st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 )

hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A8, TOPDIM_1:16; :: thesis: verum

end;A8: for p being Point of [:TM1,TM2:]

for U being open Subset of [:TM1,TM2:] st p in U holds

ex W being open Subset of [:TM1,TM2:] st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 )

proof

then
[:TM1,TM2:] is finite-ind
by TOPDIM_1:15;
let p be Point of [:TM1,TM2:]; :: thesis: for U being open Subset of [:TM1,TM2:] st p in U holds

ex W being open Subset of [:TM1,TM2:] st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 )

let U be open Subset of [:TM1,TM2:]; :: thesis: ( p in U implies ex W being open Subset of [:TM1,TM2:] st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 ) )

consider F being Subset-Family of [:TM1,TM2:] such that

A9: U = union F and

A10: for e being set st e in F holds

ex X1 being Subset of TM1 ex X2 being Subset of TM2 st

( e = [:X1,X2:] & X1 is open & X2 is open ) by BORSUK_1:5;

assume p in U ; :: thesis: ex W being open Subset of [:TM1,TM2:] st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 )

then consider U12 being set such that

A11: p in U12 and

A12: U12 in F by A9, TARSKI:def 4;

A13: U12 c= U by A9, A12, ZFMISC_1:74;

consider U1 being Subset of TM1, U2 being Subset of TM2 such that

A14: U12 = [:U1,U2:] and

A15: U1 is open and

A16: U2 is open by A10, A12;

consider p1, p2 being object such that

A17: p1 in U1 and

A18: p2 in U2 and

A19: p = [p1,p2] by A11, A14, ZFMISC_1:def 2;

reconsider p1 = p1 as Point of TM1 by A17;

consider W1 being open Subset of TM1 such that

A20: p1 in W1 and

A21: W1 c= U1 and

Fr W1 is finite-ind and

A22: ind (Fr W1) <= i1 - 1 by A15, A17, TOPDIM_1:16;

set ClW1 = Cl W1;

A23: ( ind (TM1 | (Cl W1)) = ind (Cl W1) & ind (Cl W1) <= i1 ) by TOPDIM_1:17, TOPDIM_1:19;

reconsider p2 = p2 as Point of TM2 by A18;

consider W2 being open Subset of TM2 such that

A24: p2 in W2 and

A25: W2 c= U2 and

Fr W2 is finite-ind and

A26: ind (Fr W2) <= i2 - 1 by A16, A18, TOPDIM_1:16;

reconsider W12 = [:W1,W2:] as open Subset of [:TM1,TM2:] by BORSUK_1:6;

take W12 ; :: thesis: ( p in W12 & W12 c= U & Fr W12 is finite-ind & ind (Fr W12) <= (i1 + i2) - 1 )

W12 c= U12 by A14, A25, A21, ZFMISC_1:96;

hence ( p in W12 & W12 c= U ) by A13, A19, A24, A20, ZFMISC_1:87; :: thesis: ( Fr W12 is finite-ind & ind (Fr W12) <= (i1 + i2) - 1 )

((i1 + i2) + 1) + 1 <= n + 1 by A4;

then A27: (i1 + i2) + 1 <= n by XREAL_1:6;

set FrW1 = Fr W1;

A28: ind (TM1 | (Fr W1)) = ind (Fr W1) by TOPDIM_1:17;

set ClW2 = Cl W2;

reconsider F1C2 = [:(Fr W1),(Cl W2):] as Subset of [:TM1,TM2:] ;

A29: [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] = [:TM1,TM2:] | F1C2 by BORSUK_3:22;

( ind (TM2 | (Cl W2)) = ind (Cl W2) & ind (Cl W2) <= i2 ) by TOPDIM_1:17, TOPDIM_1:19;

then A30: (ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2))) <= (i1 - 1) + i2 by A22, A28, XREAL_1:7;

then ((ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2)))) + 2 <= ((i1 + i2) - 1) + 2 by XREAL_1:6;

then A31: ( W2 c= Cl W2 & ((ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2)))) + 2 <= n ) by A27, PRE_TOPC:18, XXREAL_0:2;

then [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] is finite-ind by A2, A7, A24;

then A32: F1C2 is finite-ind by A29, TOPDIM_1:18;

set FrW2 = Fr W2;

reconsider C1F2 = [:(Cl W1),(Fr W2):] as Subset of [:TM1,TM2:] ;

A33: [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] = [:TM1,TM2:] | C1F2 by BORSUK_3:22;

ind (TM2 | (Fr W2)) = ind (Fr W2) by TOPDIM_1:17;

then A34: (ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2))) <= i1 + (i2 - 1) by A26, A23, XREAL_1:7;

then ((ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2)))) + 2 <= (i1 + (i2 - 1)) + 2 by XREAL_1:6;

then A35: ((ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2)))) + 2 <= n by A27, XXREAL_0:2;

( W1 c= Cl W1 & [#] (TM1 | (Cl W1)) = Cl W1 ) by PRE_TOPC:18, PRE_TOPC:def 5;

then A36: not TM1 | (Cl W1) is empty by A20;

then [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] is finite-ind by A2, A35;

then A37: C1F2 is finite-ind by A33, TOPDIM_1:18;

ind [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] <= (ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2))) by A2, A35, A36;

then ind [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] <= (i1 + i2) - 1 by A34, XXREAL_0:2;

then A38: ind C1F2 <= (i1 + i2) - 1 by A33, A37, TOPDIM_1:17;

A39: ( F1C2 is closed & [:TM1,TM2:] | (C1F2 \/ F1C2) is second-countable ) by TOPALG_3:15;

ind [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] <= (ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2))) by A2, A7, A24, A31;

then ind [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] <= (i1 - 1) + i2 by A30, XXREAL_0:2;

then ind F1C2 <= (i1 + i2) - 1 by A29, A32, TOPDIM_1:17;

then ( C1F2 \/ F1C2 is finite-ind & ind (C1F2 \/ F1C2) <= (i1 + i2) - 1 ) by A39, A32, A37, A38, Th5;

hence ( Fr W12 is finite-ind & ind (Fr W12) <= (i1 + i2) - 1 ) by Th10; :: thesis: verum

end;ex W being open Subset of [:TM1,TM2:] st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 )

let U be open Subset of [:TM1,TM2:]; :: thesis: ( p in U implies ex W being open Subset of [:TM1,TM2:] st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 ) )

consider F being Subset-Family of [:TM1,TM2:] such that

A9: U = union F and

A10: for e being set st e in F holds

ex X1 being Subset of TM1 ex X2 being Subset of TM2 st

( e = [:X1,X2:] & X1 is open & X2 is open ) by BORSUK_1:5;

assume p in U ; :: thesis: ex W being open Subset of [:TM1,TM2:] st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 )

then consider U12 being set such that

A11: p in U12 and

A12: U12 in F by A9, TARSKI:def 4;

A13: U12 c= U by A9, A12, ZFMISC_1:74;

consider U1 being Subset of TM1, U2 being Subset of TM2 such that

A14: U12 = [:U1,U2:] and

A15: U1 is open and

A16: U2 is open by A10, A12;

consider p1, p2 being object such that

A17: p1 in U1 and

A18: p2 in U2 and

A19: p = [p1,p2] by A11, A14, ZFMISC_1:def 2;

reconsider p1 = p1 as Point of TM1 by A17;

consider W1 being open Subset of TM1 such that

A20: p1 in W1 and

A21: W1 c= U1 and

Fr W1 is finite-ind and

A22: ind (Fr W1) <= i1 - 1 by A15, A17, TOPDIM_1:16;

set ClW1 = Cl W1;

A23: ( ind (TM1 | (Cl W1)) = ind (Cl W1) & ind (Cl W1) <= i1 ) by TOPDIM_1:17, TOPDIM_1:19;

reconsider p2 = p2 as Point of TM2 by A18;

consider W2 being open Subset of TM2 such that

A24: p2 in W2 and

A25: W2 c= U2 and

Fr W2 is finite-ind and

A26: ind (Fr W2) <= i2 - 1 by A16, A18, TOPDIM_1:16;

reconsider W12 = [:W1,W2:] as open Subset of [:TM1,TM2:] by BORSUK_1:6;

take W12 ; :: thesis: ( p in W12 & W12 c= U & Fr W12 is finite-ind & ind (Fr W12) <= (i1 + i2) - 1 )

W12 c= U12 by A14, A25, A21, ZFMISC_1:96;

hence ( p in W12 & W12 c= U ) by A13, A19, A24, A20, ZFMISC_1:87; :: thesis: ( Fr W12 is finite-ind & ind (Fr W12) <= (i1 + i2) - 1 )

((i1 + i2) + 1) + 1 <= n + 1 by A4;

then A27: (i1 + i2) + 1 <= n by XREAL_1:6;

set FrW1 = Fr W1;

A28: ind (TM1 | (Fr W1)) = ind (Fr W1) by TOPDIM_1:17;

set ClW2 = Cl W2;

reconsider F1C2 = [:(Fr W1),(Cl W2):] as Subset of [:TM1,TM2:] ;

A29: [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] = [:TM1,TM2:] | F1C2 by BORSUK_3:22;

( ind (TM2 | (Cl W2)) = ind (Cl W2) & ind (Cl W2) <= i2 ) by TOPDIM_1:17, TOPDIM_1:19;

then A30: (ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2))) <= (i1 - 1) + i2 by A22, A28, XREAL_1:7;

then ((ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2)))) + 2 <= ((i1 + i2) - 1) + 2 by XREAL_1:6;

then A31: ( W2 c= Cl W2 & ((ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2)))) + 2 <= n ) by A27, PRE_TOPC:18, XXREAL_0:2;

then [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] is finite-ind by A2, A7, A24;

then A32: F1C2 is finite-ind by A29, TOPDIM_1:18;

set FrW2 = Fr W2;

reconsider C1F2 = [:(Cl W1),(Fr W2):] as Subset of [:TM1,TM2:] ;

A33: [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] = [:TM1,TM2:] | C1F2 by BORSUK_3:22;

ind (TM2 | (Fr W2)) = ind (Fr W2) by TOPDIM_1:17;

then A34: (ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2))) <= i1 + (i2 - 1) by A26, A23, XREAL_1:7;

then ((ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2)))) + 2 <= (i1 + (i2 - 1)) + 2 by XREAL_1:6;

then A35: ((ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2)))) + 2 <= n by A27, XXREAL_0:2;

( W1 c= Cl W1 & [#] (TM1 | (Cl W1)) = Cl W1 ) by PRE_TOPC:18, PRE_TOPC:def 5;

then A36: not TM1 | (Cl W1) is empty by A20;

then [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] is finite-ind by A2, A35;

then A37: C1F2 is finite-ind by A33, TOPDIM_1:18;

ind [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] <= (ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2))) by A2, A35, A36;

then ind [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] <= (i1 + i2) - 1 by A34, XXREAL_0:2;

then A38: ind C1F2 <= (i1 + i2) - 1 by A33, A37, TOPDIM_1:17;

A39: ( F1C2 is closed & [:TM1,TM2:] | (C1F2 \/ F1C2) is second-countable ) by TOPALG_3:15;

ind [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] <= (ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2))) by A2, A7, A24, A31;

then ind [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] <= (i1 - 1) + i2 by A30, XXREAL_0:2;

then ind F1C2 <= (i1 + i2) - 1 by A29, A32, TOPDIM_1:17;

then ( C1F2 \/ F1C2 is finite-ind & ind (C1F2 \/ F1C2) <= (i1 + i2) - 1 ) by A39, A32, A37, A38, Th5;

hence ( Fr W12 is finite-ind & ind (Fr W12) <= (i1 + i2) - 1 ) by Th10; :: thesis: verum

hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A8, TOPDIM_1:16; :: thesis: verum

proof

A43:
for n being Nat holds S
let TM1, TM2 be second-countable finite-ind metrizable TopSpace; :: thesis: ( ( not TM1 is empty or not TM2 is empty ) & ((ind TM1) + (ind TM2)) + 2 <= 0 implies ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) )

assume that

A41: ( not TM1 is empty or not TM2 is empty ) and

A42: ((ind TM1) + (ind TM2)) + 2 <= 0 ; :: thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )

reconsider i1 = (ind TM1) + 1, i2 = (ind TM2) + 1 as Nat by Lm1;

i1 + i2 <= 0 by A42;

hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A41; :: thesis: verum

end;assume that

A41: ( not TM1 is empty or not TM2 is empty ) and

A42: ((ind TM1) + (ind TM2)) + 2 <= 0 ; :: thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )

reconsider i1 = (ind TM1) + 1, i2 = (ind TM2) + 1 as Nat by Lm1;

i1 + i2 <= 0 by A42;

hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A41; :: thesis: verum

((ind TM1) + (ind TM2)) + 2 = i1 + i2 ;

hence ( ( not TM1 is empty or not TM2 is empty ) implies ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) ) by A43; :: thesis: verum