let n be Nat; :: thesis: for A being Subset of (TOP-REAL n) st A is closed & A is Bounded holds
A is compact
defpred S₁[ Nat] means for A being Subset of (TOP-REAL $1) st A is closed & A is Bounded holds
A is compact ;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: S₁[n + 1]

hence S₁[n + 1] by Lm4; :: thesis: verum

end;

suppose A3: n <> 0 ; :: thesis: S₁[n + 1]

set n1 = n + 1;
set TR1 = TOP-REAL 1;
set TRn = TOP-REAL n;
set TRn1 = TOP-REAL (n + 1);
let A be Subset of (TOP-REAL (n + 1)); :: thesis: ( A is closed & A is Bounded implies A is compact )
assume that
A4: A is closed and
A5: A is Bounded ; :: thesis: A is compact
consider p being Point of (Euclid (n + 1)), r being real number such that
A6: A c= OpenHypercube (p,r) by A5, Th21;
A7: n in NAT by ORDINAL1:def 12;
then consider f being Function of [:(TOP-REAL n),(TOP-REAL 1):],(TOP-REAL (n + 1)) such that
A8: f is being_homeomorphism and
A9: for fi being Element of (TOP-REAL n)
for fj being Element of (TOP-REAL 1) holds f . (fi,fj) = fi ^ fj by Th19;
A10: ( f is one-to-one & dom f = [#] [:(TOP-REAL n),(TOP-REAL 1):] ) by A8, TOPGRP_1:24;
len p = n + 1 by CARD_1:def 7;
then consider q1, q2 being FinSequence such that
A11: len q1 = n and
A12: len q2 = 1 and
A13: p = q1 ^ q2 by FINSEQ_2:22;
rng p c= REAL ;
then A14: p is FinSequence of REAL by FINSEQ_1:def 4;
then A15: q1 is FinSequence of REAL by A13, FINSEQ_1:36;
A16: q2 is FinSequence of REAL by A13, A14, FINSEQ_1:36;
reconsider q1 = q1 as Element of (Euclid n) by A11, A15, TOPREAL7:16;
reconsider q2 = q2 as Element of (Euclid 1) by A12, A16, TOPREAL7:16;
A17: f is continuous by A8, TOPS_2:def 5;
reconsider Bn = cl_Ball (q1,(r * (sqrt n))) as Subset of (TOP-REAL n) by TOPREAL3:8;
reconsider B1 = cl_Ball (q2,(r * (sqrt 1))) as Subset of (TOP-REAL 1) by TOPREAL3:8;
( Ball (q2,(r * (sqrt 1))) c= B1 & OpenHypercube (q2,r) c= Ball (q2,(r * (sqrt 1))) ) by EUCLID_9:18, METRIC_1:14;
then A18: OpenHypercube (q2,r) c= B1 by XBOOLE_1:1;
( Ball (q1,(r * (sqrt n))) c= Bn & OpenHypercube (q1,r) c= Ball (q1,(r * (sqrt n))) ) by A3, EUCLID_9:18, METRIC_1:14;
then OpenHypercube (q1,r) c= Bn by XBOOLE_1:1;
then A19: [:(OpenHypercube (q1,r)),(OpenHypercube (q2,r)):] c= [:Bn,B1:] by A18, ZFMISC_1:96;
cl_Ball (q2,(r * (sqrt 1))) is bounded by TOPREAL6:59;
then B1 is Bounded by JORDAN2C:def 1;
then A20: B1 is compact by Lm4, TOPREAL6:58;
cl_Ball (q1,(r * (sqrt n))) is bounded by TOPREAL6:59;
then Bn is Bounded by JORDAN2C:def 1;
then Bn is compact by A2, A7, TOPREAL6:58;
then A21: [:Bn,B1:] is compact Subset of [:(TOP-REAL n),(TOP-REAL 1):] by A20, BORSUK_3:23;
rng f = [#] (TOP-REAL (n + 1)) by A8, TOPGRP_1:24;
then A22: f .: (f " A) = A by FUNCT_1:77;
f .: [:(OpenHypercube (q1,r)),(OpenHypercube (q2,r)):] = OpenHypercube (p,r) by A9, A11, A13, Th20;
then A23: f " A c= [:(OpenHypercube (q1,r)),(OpenHypercube (q2,r)):] by A6, A10, A22, FUNCT_1:87;
f " A is closed by A4, A8, TOPGRP_1:24;
then f " A is compact by A19, A21, A23, COMPTS_1:9, XBOOLE_1:1;
hence A is compact by A17, A22, WEIERSTR:8; :: thesis: verum

end;

end;

end;

A24: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A24, A1);
hence for A being Subset of (TOP-REAL n) st A is closed & A is Bounded holds
A is compact ; :: thesis: verum