0 & Ball(pe,r) c= P proof let pe be Point of Euclid n; assume pe in P; then consider p such that A3: p=pe and A4: s1

0 by A4,XREAL_1:50;
Ball(pe,r) c= P
proof
let x be object;
assume x in Ball(pe,r);
then x in {q where q is Element of Euclid n:dist(pe,q)~~0 & P=Ball(u,r) holds f1"P is open
proof
let r be Real, u be Element of RealSpace, P be
Subset of TopSpaceMetr RealSpace;
assume that
r>0 and
A3: P=Ball(u,r);
reconsider u1=u as Real;
Ball(u,r)={s:u1-r~~~~=<*|.s.|*>
proof
let s be Real;
reconsider s as Element of REAL by XREAL_0:def 1;
rng <*s*> c= dom absreal
proof
let x be object;
assume x in rng <*s*>;
then x in {s} by FINSEQ_1:38;
then
A1: x=s by TARSKI:def 1;
dom absreal =REAL by FUNCT_2:def 1;
hence thesis by A1;
end;
then dom <*s*>=dom (absreal*<*s*>) by RELAT_1:27;
then Seg 1=dom (abs <*s*>) by FINSEQ_1:def 8;
then
A2: len (abs <*s*>)=1 by FINSEQ_1:def 3;
A3: len <*|.s.|*>=1 by FINSEQ_1:39;
for j be Nat st 1<=j & j<=len <*|.s.|*> holds <*|.s.|*>.j=(abs <*s*>) .j
proof
let j be Nat;
A4: <*s*>.1=s & <*s*> is Element of REAL 1 by FINSEQ_1:40,FINSEQ_2:98;
assume 1<=j & j<=len <*|.s.|*>;
then
A5: j=1 by A3,XXREAL_0:1;
then <*|.s.|*>.j =|.s.| by FINSEQ_1:40;
hence thesis by A5,A4,VALUED_1:18;
end;
hence thesis by A2,A3,FINSEQ_1:14;
end;
theorem Th20:
for p being Element of TOP-REAL 1 ex r being Real st p=<*r*>
proof
let p be Element of TOP-REAL 1;
1-tuples_on REAL = REAL 1;
then reconsider p9=p as Element of 1-tuples_on REAL by EUCLID:22;
ex r be Element of REAL st p9=<*r*> by FINSEQ_2:97;
hence thesis;
end;
notation
let r be Real;
synonym |[ r ]| for <*r*>;
end;
definition
let r be Real;
redefine func |[ r ]| -> Point of TOP-REAL 1;
coherence
proof
reconsider r as Element of REAL by XREAL_0:def 1;
<*r*> in REAL 1 by FINSEQ_2:98;
hence thesis by EUCLID:22;
end;
end;
theorem
s*|[ r ]|=|[ s*r ]| by RVSUM_1:47;
theorem
|[ r1+r2 ]|=|[ r1 ]|+|[ r2 ]| by RVSUM_1:13;
theorem
|[r1]|=|[r2]| implies r1=r2 by FINSEQ_1:76;
theorem Th24:
for P being Subset of R^1,b being Real st P = { s: s~~** 0
& Ball(c,r) c= P
proof
let c be Point of RealSpace;
reconsider n = c as Element of REAL by METRIC_1:def 13;
reconsider r = b-n as Element of REAL by XREAL_0:def 1;
assume c in P;
then
A2: ex s st s=n & s 0
& Ball(c,r) c= P
proof
let c be Point of RealSpace;
reconsider n = c as Element of REAL by METRIC_1:def 13;
reconsider r = n-a as Real;
assume c in P;
then
A2: ex s st s=n & a**