let n be Nat; ( TOP-REAL n is finite-ind & ind (TOP-REAL n) <= n )
defpred S1[ Nat] means ( TOP-REAL $1 is finite-ind & ind (TOP-REAL $1) <= $1 );
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
A2:
(
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
= TopSpaceMetr (Euclid n) &
TopStruct(# the
carrier of
(TOP-REAL (n + 1)), the
topology of
(TOP-REAL (n + 1)) #)
= TopSpaceMetr (Euclid (n + 1)) &
TopStruct(# the
carrier of
(TOP-REAL 1), the
topology of
(TOP-REAL 1) #)
= TopSpaceMetr (Euclid 1) )
by EUCLID:def 8;
A3:
n in NAT
by ORDINAL1:def 12;
then A4:
[:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid 1)):],
TopSpaceMetr (Euclid (n + 1)) are_homeomorphic
by TOPREAL7:25;
TOP-REAL 1,
TopSpaceMetr (Euclid 1) are_homeomorphic
by A2, YELLOW14:19;
then A5:
(
TopSpaceMetr (Euclid 1) is
finite-ind &
ind (TopSpaceMetr (Euclid 1)) = 1 )
by Lm8, TOPDIM_1:24, TOPDIM_1:25;
assume A6:
S1[
n]
;
S1[n + 1]
A7:
TOP-REAL n,
TopSpaceMetr (Euclid n) are_homeomorphic
by A2, YELLOW14:19;
A8:
TOP-REAL (n + 1),
TopSpaceMetr (Euclid (n + 1)) are_homeomorphic
by A2, YELLOW14:19;
A9:
(
TopSpaceMetr (Euclid n) is
finite-ind &
ind (TopSpaceMetr (Euclid n)) = ind (TOP-REAL n) )
by A6, A7, TOPDIM_1:24, TOPDIM_1:25;
then A10:
ind [:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid 1)):] <= (ind (TopSpaceMetr (Euclid n))) + 1
by Lm5, A2, A5;
(ind (TopSpaceMetr (Euclid n))) + 1
<= n + 1
by A6, A9, XREAL_1:6;
then
ind [:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid 1)):] <= n + 1
by A10, XXREAL_0:2;
then A11:
ind (TopSpaceMetr (Euclid (n + 1))) <= n + 1
by A3, A9, A5, A2, TOPDIM_1:25, TOPREAL7:25;
TopSpaceMetr (Euclid (n + 1)) is
finite-ind
by A9, A5, A2, A4, TOPDIM_1:24;
then
TOP-REAL (n + 1) is
finite-ind
by A8, TOPDIM_1:24;
hence
S1[
n + 1]
by A11, A2, TOPDIM_1:25, YELLOW14:19;
verum
end;
A12:
S1[ 0 ]
by Lm7;
for n being Nat holds S1[n]
from NAT_1:sch 2(A12, A1);
hence
( TOP-REAL n is finite-ind & ind (TOP-REAL n) <= n )
; verum