:: On Some Properties of Real {H}ilbert Space, {II}
:: by Hiroshi Yamazaki , Yasumasa Suzuki , Takao Inou\'e and Yasunari Shidama
::
:: Received April 17, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, BHSP_1, PRE_TOPC, REAL_1, COMPLEX1, ARYTM_1, ARYTM_3,
XXREAL_0, CARD_1, SUBSET_1, RELAT_1, HAHNBAN, BHSP_6, FINSET_1, XBOOLE_0,
TARSKI, BHSP_5, STRUCT_0, BINOP_2, FUNCT_1, ZFMISC_1, NAT_1, SEQ_2,
ALGSTR_0, BINOP_1, SETWISEO, PROB_2, FINSEQ_1, FINSOP_1, SQUARE_1,
NORMSP_1, SEMI_AF1, SUPINF_2, RSSPACE2;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, BINOP_2, STRUCT_0, ALGSTR_0, NORMSP_0, COMPLEX1, REAL_1, NAT_1,
FUNCT_1, FUNCT_2, RELAT_1, PRE_TOPC, BHSP_1, SQUARE_1, SEQ_2, BINOP_1,
FINSET_1, SETWISEO, HAHNBAN, FINSEQ_1, FINSOP_1, BHSP_5, BHSP_6,
RSSPACE2, PARTFUN1, XXREAL_0;
constructors BINOP_1, DOMAIN_1, SETWISEO, REAL_1, SQUARE_1, BINOP_2, COMPLEX1,
FINSOP_1, BHSP_3, BHSP_5, BHSP_6, RELSET_1, COMSEQ_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1,
NUMBERS, XREAL_0, BINOP_2, STRUCT_0, BHSP_5, SQUARE_1, NAT_1, VALUED_0;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI;
equalities SQUARE_1, RLVECT_1;
expansions TARSKI;
theorems XBOOLE_1, SQUARE_1, ZFMISC_1, ABSVALUE, FUNCT_1, NAT_1, FUNCT_2,
RLVECT_1, SEQ_2, SEQ_4, BHSP_1, BHSP_5, BHSP_6, UNIFORM1, CHAIN_1,
XCMPLX_1, BINOP_2, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1;
schemes NAT_1, FUNCT_2;
begin :: Necessary and sufficient condition for summable set
reserve X for RealUnitarySpace;
reserve x, y, y1, y2 for Point of X;
Lm1: for x, y, z, e be Real
holds |.x-y.| < e/2 & |.y-z.| < e/2 implies |.x-z.| <e
proof
let x, y, z, e be Real;
assume |.x-y.| < e/2 & |.y-z.| <e/2;
then |.(x-y)+(y-z).| <= |.x-y.|+|.y-z.| & |.x-y.|+|.y-z.| < e/2+e/2 by
COMPLEX1:56,XREAL_1:8;
hence thesis by XXREAL_0:2;
end;
Lm2: for p being Real st p > 0
ex k be Nat st 1/(k+1) < p
proof
let p be Real;
consider k1 be Nat such that
A1: p" < k1 by SEQ_4:3;
assume p > 0;
then
A2: 0 < p";
take k1;
p"+0 < k1+1 by A1,XREAL_1:8;
then 1/(k1+1) < 1/p" by A2,XREAL_1:76;
hence thesis by XCMPLX_1:216;
end;
Lm3: for p being Real, m being Nat st p > 0
ex i be Nat st 1/(i+1) < p & i >= m
proof
let p be Real, m be Nat;
consider k1 be Nat such that
A1: p"<k1 by SEQ_4:3;
assume p > 0;
then
A2: 0<p";
reconsider i = k1+m as Nat;
take i;
k1 <= k1 + m by NAT_1:11;
then p" < i by A1,XXREAL_0:2;
then p"+0 < i+1 by XREAL_1:8;
then 1/(i+1) < 1/p" by A2,XREAL_1:76;
hence thesis by NAT_1:11,XCMPLX_1:216;
end;
theorem Th1:
for Y be Subset of X for L be Functional of X holds Y
is_summable_set_by L iff for e be Real st 0 < e holds ex Y0 be finite Subset of
X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y1 is non
empty & Y1 c= Y & Y0 misses Y1 holds |.setopfunc(Y1, the carrier of X, REAL,
L, addreal).| <e
proof
let Y be Subset of X;
let L be Functional of X;
thus Y is_summable_set_by L implies for e be Real st 0 < e holds ex Y0 be
finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X
st Y1 is non empty & Y1 c= Y & Y0 misses Y1 holds |.setopfunc(Y1, the carrier
of X, REAL, L, addreal).| <e
proof
assume Y is_summable_set_by L;
then consider r be Real such that
A1: for e be Real
st e > 0 ex Y0 be finite Subset of X st Y0 is non
empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds |.
r - setopfunc(Y1, the carrier of X, REAL, L, addreal).| < e
by BHSP_6:def 6;
for e be Real st 0 < e
ex Y0 be finite Subset of X st Y0 is non
empty & Y0 c= Y & for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y &
Y0 misses Y1 holds |.setopfunc(Y1, the carrier of X, REAL, L, addreal).| <e
proof
let e be Real;
assume 0 < e;
then consider Y0 be finite Subset of X such that
A2: Y0 is non empty and
A3: Y0 c= Y and
A4: for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds |.r -
setopfunc(Y1, the carrier of X, REAL, L, addreal).| < e/2 by A1,XREAL_1:139;
for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & Y0
misses Y1 holds |.setopfunc(Y1, the carrier of X, REAL, L, addreal).| < e
proof
let Y1 be finite Subset of X such that
Y1 is non empty and
A5: Y1 c= Y and
A6: Y0 misses Y1;
set Y19 = Y0 \/ Y1;
dom L = the carrier of X by FUNCT_2:def 1;
then setopfunc(Y19, the carrier of X, REAL, L, addreal) = addreal.(
setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y1, the carrier of
X, REAL, L, addreal)) by A6,BHSP_5:14
.= setopfunc(Y0, the carrier of X, REAL, L, addreal) + setopfunc(
Y1, the carrier of X, REAL, L, addreal) by BINOP_2:def 9;
then
A7: setopfunc(Y1, the carrier of X, REAL, L, addreal) = setopfunc(Y19
, the carrier of X, REAL, L, addreal) - setopfunc(Y0, the carrier of X, REAL, L
, addreal);
Y0 c= Y19 by XBOOLE_1:7;
then
|.r - setopfunc(Y19, the carrier of X, REAL, L, addreal).| < e/2
by A3,A4,A5,XBOOLE_1:8;
then
A8: |.setopfunc(Y19, the carrier of X, REAL, L, addreal)-r.| < e/2
by UNIFORM1:11;
|.r - setopfunc(Y0, the carrier of X, REAL, L, addreal).| < e/2
by A3,A4;
hence thesis by A8,A7,Lm1;
end;
hence thesis by A2,A3;
end;
hence thesis;
end;
assume
A9: for e be Real st 0 < e holds ex Y0 be finite Subset of X st Y0 is
non empty & Y0 c= Y & for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y
& Y0 misses Y1 holds |.setopfunc(Y1, the carrier of X, REAL, L, addreal).| <e;
ex r be Real st
for e be Real st 0 < e ex Y0 be finite Subset of X st
Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y
holds |.r - setopfunc(Y1, the carrier of X, REAL, L, addreal).| < e
proof
defpred P[object,object] means
ex D2 being set st D2 = $2 &
$2 is finite Subset of X & D2 is non empty & D2
c= Y & for z be Real st z=$1 for Y1 be finite Subset of X st Y1 is non empty &
Y1 c= Y & D2 misses Y1 holds |.setopfunc(Y1, the carrier of X, REAL, L,
addreal).| < 1/(z+1);
A10: for x be object st x in NAT ex y be object st y in bool Y & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider xx = x as Element of NAT;
reconsider e = 1/(xx+1) as Real;
0/(xx + 1) < 1/(xx + 1) by XREAL_1:74;
then consider Y0 be finite Subset of X such that
A11: Y0 is non empty and
A12: Y0 c= Y & for Y1 be finite Subset of X st Y1 is non empty & Y1
c= Y & Y0 misses Y1 holds |.setopfunc(Y1, the carrier of X, REAL, L, addreal)
.| < e by A9;
take Y0;
thus Y0 in bool Y by A12,ZFMISC_1:def 1;
take D2 = Y0;
thus D2 = Y0;
thus Y0 is finite Subset of X;
thus D2 is non empty by A11;
thus D2 c= Y by A12;
for z be Real st z = x for Y1 be finite Subset of X
st Y1 is non empty & Y1 c= Y & Y0 misses Y1 holds |.setopfunc(Y1, the carrier
of X, REAL, L, addreal).| < 1/(z+1) by A12;
hence
for z be Real st z=x
for Y1 be finite Subset of X st Y1 is non
empty & Y1 c= Y & D2 misses Y1 holds |.setopfunc(Y1, the carrier of X, REAL, L
, addreal).| < 1/(z+1);
end;
A13: ex B being sequence of bool Y st
for x be object st x in NAT holds P[x,B. x] from FUNCT_2:sch 1(A10);
ex A be sequence of bool Y st for i be Nat holds A.i
is finite Subset of X & A.i is non empty & A.i c= Y & (for Y1 be finite Subset
of X st Y1 is non empty & Y1 c= Y & A.i misses Y1 holds |.setopfunc(Y1, the
carrier of X, REAL, L, addreal).| < 1/(i+1)) & for j be Element of NAT
st i <= j
holds A.i c= A.j
proof
consider B being sequence of bool Y such that
A14: for x be object st x in NAT holds P[x,B. x] by A13;
A15: for x be object st x in NAT
holds B.x is finite Subset of X & B.x
is non empty & B.x c= Y & for z be Real st z=x for Y1 be finite Subset of X st
Y1 is non empty & Y1 c= Y & B.x misses Y1 holds |.setopfunc(Y1, the carrier
of X, REAL, L, addreal).| < 1/(z+1)
proof let x be object such that
A16: x in NAT;
P[x,B.x] by A16,A14;
hence B.x is finite Subset of X &
B.x is non empty & B.x c= Y &
for z be Real st z=x for Y1 be finite Subset of X st
Y1 is non empty & Y1 c= Y & B.x misses Y1 holds |.setopfunc(Y1, the carrier
of X, REAL, L, addreal).| < 1/(z+1);
end;
deffunc G(Nat,set) = B.($1+1) \/ $2;
ex A being Function st dom A = NAT & A.0 = B.0 & for n being Nat
holds A.(n+1) = G(n,A.n) from NAT_1:sch 11;
then consider A being Function such that
A17: dom A = NAT and
A18: A.0 = B.0 and
A19: for n being Nat holds A.(n+1) = B.(n+1) \/ A.n;
defpred R[Nat] means
A.$1 is finite Subset of X & A.$1 is non
empty & A.$1 c= Y & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y
& A.$1 misses Y1 holds |.setopfunc(Y1, the carrier of X, REAL, L, addreal).| <
1/($1+1)) & for j be Element of NAT st $1 <= j holds A.$1 c= A.j;
A20: now
let n be Nat such that
A21: R[n];
A22: for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & A.(n+
1) misses Y1 holds |.setopfunc(Y1, the carrier of X, REAL, L, addreal).| < 1/(
(n+1)+1)
proof
let Y1 be finite Subset of X such that
A23: Y1 is non empty & Y1 c= Y and
A24: A.(n+1) misses Y1;
A.(n+1) = B.(n+1) \/ A.n by A19;
then B.(n+1) misses Y1 by A24,XBOOLE_1:7,63;
hence thesis by A15,A23;
end;
defpred P[Nat] means n+1 <= $1 implies A.(n+1) c= A.$1;
A25: for j being Nat st P[j] holds P[j+1]
proof
let j be Nat such that
A26: P[j] and
A27: n+1 <= j+1;
now
per cases;
case
n = j;
hence thesis;
end;
case
A28: n <> j;
A.(j+1) = (B.(j+1) \/ A.j) by A19;
then
A29: A.j c= A.(j+1) by XBOOLE_1:7;
n <= j by A27,XREAL_1:6;
then n < j by A28,XXREAL_0:1;
hence thesis by A26,A29,NAT_1:13;
end;
end;
hence thesis;
end;
A30: P[0];
A31: for j be Nat holds P[j] from NAT_1:sch 2(A30, A25);
A.(n+1) = B.(n+1) \/ A.n & B.(n+1) is finite Subset of X by A15,A19;
hence R[n+1] by A21,A22,A31,XBOOLE_1:8;
end;
for j0 be Nat st j0=0 holds for j be Nat st j0 <= j holds A.j0 c= A.j
proof
let j0 be Nat such that
A32: j0 = 0;
defpred P[Nat] means j0 <= $1 implies A.j0 c= A.$1;
A33: now
let j be Nat such that
A34: P[j];
A.(j+1) = (B.(j+1) \/ A.j) by A19;
then A.j c= A.(j+1) by XBOOLE_1:7;
hence P[j+1] by A32,A34,XBOOLE_1:1;
end;
A35: P[0] by A32;
thus for j be Nat holds P[j] from NAT_1:sch 2(A35, A33 );
end;
then
A36: R[0] by A15,A18;
A37: for i be Nat holds R[i] from NAT_1:sch 2(A36,A20);
rng A c= bool Y
proof
let y be object;
assume y in rng A;
then consider x be object such that
A38: x in dom A and
A39: y = A.x by FUNCT_1:def 3;
reconsider i = x as Element of NAT by A17,A38;
A.i c= Y by A37;
hence thesis by A39,ZFMISC_1:def 1;
end;
then A is sequence of bool Y by A17,FUNCT_2:2;
hence thesis by A37;
end;
then consider A be sequence of bool Y such that
A40: for i be Nat holds A.i is finite Subset of X & A.i is
non empty & A.i c= Y & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c=
Y & A.i misses Y1 holds |.setopfunc(Y1, the carrier of X, REAL, L, addreal).|<
1/(i+1)) & for j be Element of NAT st i <= j holds A.i c= A.j;
defpred P[object,object] means
ex Y1 be finite Subset of X st Y1 is non empty &
A.$1 = Y1 & $2 = setopfunc(Y1, the carrier of X, REAL, L, addreal);
A41: for x be object st x in NAT ex y be object st y in REAL & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider i=x as Element of NAT;
A.i is finite Subset of X by A40;
then reconsider Y1 = A.x as finite Subset of X;
reconsider y = setopfunc(Y1, the carrier of X, REAL, L, addreal) as set;
A.i is non empty by A40;
then ex Y1 be finite Subset of X st Y1 is non empty & A.x = Y1 & y =
setopfunc(Y1, the carrier of X, REAL, L, addreal);
hence thesis;
end;
ex F being sequence of REAL st for x be object st x in NAT
holds P[x,F.x] from FUNCT_2:sch 1(A41);
then consider F being sequence of REAL such that
A42: for x be object st x in NAT holds ex Y1 be finite Subset of X st Y1
is non empty & A.x = Y1 & F.x = setopfunc(Y1, the carrier of X, REAL, L,
addreal);
set seq = F;
A43: for e be Real st e > 0 ex k be Nat st
for n, m be Nat st n >= k & m >= k
holds |.(seq.n) - ((seq.m) qua Real).| < e
proof
let e be Real such that
A44: e > 0;
A45: e/2 > 0/2 by A44,XREAL_1:74;
then consider k be Nat such that
A46: 1/(k+1) < e/2 by Lm2;
take k;
let nn, mm be Nat such that
A47: nn >= k and
A48: mm >= k;
reconsider m=mm, n=nn, k as Element of NAT by ORDINAL1:def 12;
consider Y2 be finite Subset of X such that
Y2 is non empty and
A49: A.m = Y2 and
A50: seq.m = setopfunc(Y2, the carrier of X, REAL, L, addreal) by A42;
consider Y0 be finite Subset of X such that
Y0 is non empty and
A51: A.k = Y0 and
seq.k = setopfunc(Y0, the carrier of X, REAL, L, addreal) by A42;
A52: Y0 c= Y2 by A40,A48,A51,A49;
consider Y1 be finite Subset of X such that
Y1 is non empty and
A53: A.n = Y1 and
A54: seq.n = setopfunc(Y1, the carrier of X, REAL, L, addreal) by A42;
A55: Y0 c= Y1 by A40,A47,A51,A53;
now
per cases;
case
A56: Y0 = Y1;
now
per cases;
case
Y0 = Y2;
hence thesis by A44,A54,A50,A56,ABSVALUE:2;
end;
case
A57: Y0 <> Y2;
ex Y02 be finite Subset of X st Y02 is non empty & Y02 c= Y
& Y02 misses Y0 & Y0 \/ Y02 = Y2
proof
take Y02 = Y2 \ Y0;
A58: Y2 \ Y0 c= Y2 by XBOOLE_1:36;
Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39
.= Y2 by A52,XBOOLE_1:12;
hence thesis by A49,A57,A58,XBOOLE_1:1,79;
end;
then consider Y02 be finite Subset of X such that
A59: Y02 is non empty & Y02 c= Y and
A60: Y02 misses Y0 and
A61: Y0 \/ Y02 = Y2;
|.setopfunc(Y02, the carrier of X, REAL, L, addreal).| <
1/(k+1) by A40,A51,A59,A60;
then
A62: |.setopfunc(Y02, the carrier of X, REAL, L, addreal).| <
e/2 by A46,XXREAL_0:2;
dom L = the carrier of X by FUNCT_2:def 1;
then setopfunc(Y2, the carrier of X, REAL, L, addreal) =
addreal.( setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y02, the
carrier of X, REAL, L, addreal)) by A60,A61,BHSP_5:14
.= setopfunc(Y0, the carrier of X, REAL, L, addreal) +
setopfunc(Y02, the carrier of X, REAL, L, addreal) by BINOP_2:def 9;
then
A63: |.(seq.n) - (seq.m).| = |.-setopfunc(Y02, the carrier
of X, REAL, L, addreal).| by A54,A50,A56
.= |.setopfunc(Y02, the carrier of X, REAL, L, addreal).|
by COMPLEX1:52;
e/2 < e by A44,XREAL_1:216;
hence thesis by A62,A63,XXREAL_0:2;
end;
end;
hence thesis;
end;
case
A64: Y0 <> Y1;
now
per cases;
case
A65: Y0 = Y2;
ex Y01 be finite Subset of X st Y01 is non empty & Y01 c=
Y & Y01 misses Y0 & Y0 \/ Y01 = Y1
proof
take Y01 = Y1 \ Y0;
A66: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A55,XBOOLE_1:12;
hence thesis by A53,A64,A66,XBOOLE_1:1,79;
end;
then consider Y01 be finite Subset of X such that
A67: Y01 is non empty & Y01 c= Y and
A68: Y01 misses Y0 and
A69: Y0 \/ Y01 = Y1;
dom L = the carrier of X by FUNCT_2:def 1;
then
A70: setopfunc(Y1, the carrier of X, REAL, L, addreal) =
addreal.( setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y01, the
carrier of X, REAL, L, addreal)) by A68,A69,BHSP_5:14
.= setopfunc(Y0, the carrier of X, REAL, L, addreal) +
setopfunc(Y01, the carrier of X, REAL, L, addreal) by BINOP_2:def 9;
|.setopfunc(Y01, the carrier of X, REAL, L, addreal).| <
1/(k+1) by A40,A51,A67,A68;
then
|.(seq.n) - (seq.m).| < e/2 by A46,A54,A50,A65,A70,XXREAL_0:2;
then |.(seq.n) - (seq.m).|+ 0 < e/2 + e/2 by A45,XREAL_1:8;
hence thesis;
end;
case
A71: Y0<>Y2;
ex Y02 be finite Subset of X st Y02 is non empty & Y02 c=
Y & Y02 misses Y0 & Y0 \/ Y02 = Y2
proof
take Y02 = Y2 \ Y0;
A72: Y2 \ Y0 c= Y2 by XBOOLE_1:36;
Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39
.= Y2 by A52,XBOOLE_1:12;
hence thesis by A49,A71,A72,XBOOLE_1:1,79;
end;
then consider Y02 be finite Subset of X such that
A73: Y02 is non empty & Y02 c= Y and
A74: Y02 misses Y0 and
A75: Y0 \/ Y02 = Y2;
dom L = the carrier of X by FUNCT_2:def 1;
then
A76: setopfunc(Y2, the carrier of X, REAL, L, addreal) =
addreal.(setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y02, the
carrier of X, REAL, L, addreal)) by A74,A75,BHSP_5:14
.= setopfunc(Y0, the carrier of X, REAL, L, addreal) +
setopfunc(Y02, the carrier of X, REAL, L, addreal) by BINOP_2:def 9;
ex Y01 be finite Subset of X st Y01 is non empty & Y01 c=
Y & Y01 misses Y0 & Y0 \/ Y01 = Y1
proof
take Y01 = Y1 \ Y0;
A77: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A55,XBOOLE_1:12;
hence thesis by A53,A64,A77,XBOOLE_1:1,79;
end;
then consider Y01 be finite Subset of X such that
A78: Y01 is non empty & Y01 c= Y and
A79: Y01 misses Y0 and
A80: Y0 \/ Y01 = Y1;
dom L = the carrier of X by FUNCT_2:def 1;
then setopfunc(Y1, the carrier of X, REAL, L, addreal) =
addreal.(setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y01, the
carrier of X, REAL, L, addreal)) by A79,A80,BHSP_5:14
.= setopfunc(Y0, the carrier of X, REAL, L, addreal) +
setopfunc(Y01, the carrier of X, REAL, L, addreal) by BINOP_2:def 9;
then seq.n - seq.m = setopfunc(Y01, the carrier of X, REAL, L,
addreal) - setopfunc(Y02, the carrier of X, REAL, L, addreal) by A54,A50,A76;
then
A81: |.(seq.n) - (seq.m).| <= |.setopfunc(Y01, the carrier
of X, REAL, L, addreal).| + |.setopfunc(Y02, the carrier of X, REAL, L,
addreal).| by COMPLEX1:57;
|.setopfunc(Y02, the carrier of X, REAL, L, addreal).| <
1/(k+1) by A40,A51,A73,A74;
then
A82: |.setopfunc(Y02, the carrier of X, REAL, L, addreal).| <
e/2 by A46,XXREAL_0:2;
|.setopfunc(Y01, the carrier of X, REAL, L, addreal).| <
1/(k+1) by A40,A51,A78,A79;
then |.setopfunc(Y01, the carrier of X, REAL, L, addreal).| <
e/2 by A46,XXREAL_0:2;
then |.setopfunc(Y01, the carrier of X, REAL, L, addreal).| +
|.setopfunc(Y02, the carrier of X, REAL, L, addreal).| < e/2 + e/2 by A82,
XREAL_1:8;
hence thesis by A81,XXREAL_0:2;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
for e be Real st 0 < e ex k be Nat st
for m be Nat st k <= m holds |.seq.m -seq.k.|<e
proof
let e be Real;
assume 0 < e;
then consider k be Nat such that
A83: for n, m be Nat st n >= k & m >= k holds |.(seq.n) - (seq.m).| < e
by A43;
for m be Nat st k <= m holds |.seq.m - seq.k.|<e by A83;
hence thesis;
end;
then seq is convergent by SEQ_4:41;
then consider x be Real such that
A84: for r be Real st r > 0 ex m be Nat st for n be
Nat st n >= m holds |.seq.n - x.| < r by SEQ_2:def 6;
reconsider r=x as Real;
take r;
for e be Real st 0 < e ex Y0 be finite Subset of X st Y0 is non
empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds |.
r - setopfunc(Y1, the carrier of X, REAL, L, addreal).| < e
proof
let e be Real;
assume e > 0;
then
A85: e/2 > 0/2 by XREAL_1:74;
then consider m be Nat such that
A86: for n be Nat st n >= m holds |.(seq.n)-r.| < e/2 by A84;
consider i be Nat such that
A87: 1/(i+1) < e/2 and
A88: i >= m by A85,Lm3;
i in NAT by ORDINAL1:def 12;
then reconsider ii=i as Element of NAT;
consider Y0 be finite Subset of X such that
A89: Y0 is non empty and
A90: A.ii = Y0 and
A91: seq.i = setopfunc(Y0, the carrier of X, REAL, L, addreal) by A42;
A92: |.setopfunc(Y0, the carrier of X, REAL, L, addreal) - r.| < e/2
by A86,A88,A91;
now
let Y1 be finite Subset of X such that
A93: Y0 c= Y1 and
A94: Y1 c= Y;
now
per cases;
case
Y0 = Y1;
then |.r - setopfunc(Y1, the carrier of X, REAL, L, addreal).| <
e/2 by A92,UNIFORM1:11;
then |.x - setopfunc(Y1, the carrier of X, REAL, L, addreal).| +
0 < e/2 + e/2 by A85,XREAL_1:8;
hence |.r - setopfunc(Y1, the carrier of X, REAL, L, addreal).| <
e;
end;
case
A95: Y0 <> Y1;
ex Y2 be finite Subset of X st Y2 is non empty & Y2 c= Y &
Y0 misses Y2 & Y0 \/ Y2 = Y1
proof
take Y2 = Y1 \ Y0;
A96: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y2 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A93,XBOOLE_1:12;
hence thesis by A94,A95,A96,XBOOLE_1:79;
end;
then consider Y2 be finite Subset of X such that
A97: Y2 is non empty & Y2 c= Y and
A98: Y0 misses Y2 and
A99: Y0 \/ Y2 = Y1;
dom L = the carrier of X by FUNCT_2:def 1;
then setopfunc(Y1, the carrier of X, REAL, L, addreal)-r =
addreal.( setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y2, the
carrier of X, REAL, L, addreal)) - r by A98,A99,BHSP_5:14
.= setopfunc(Y0, the carrier of X, REAL, L, addreal) +
setopfunc(Y2, the carrier of X, REAL, L, addreal) - r by BINOP_2:def 9
.= setopfunc(Y0, the carrier of X, REAL, L, addreal) - r +
setopfunc(Y2, the carrier of X, REAL, L, addreal);
then |.setopfunc(Y1, the carrier of X, REAL, L, addreal)-r.| <=
|.setopfunc(Y0, the carrier of X, REAL, L, addreal) - r.| + |.setopfunc(Y2,
the carrier of X, REAL, L, addreal).| by ABSVALUE:9;
then
A100: |.x - setopfunc(Y1, the carrier of X, REAL, L, addreal) .|
<= |.setopfunc(Y0, the carrier of X, REAL, L, addreal) - r.| + |.setopfunc(
Y2, the carrier of X, REAL, L, addreal).| by UNIFORM1:11;
|.setopfunc(Y2, the carrier of X, REAL, L, addreal).| < 1/(
i+1) by A40,A90,A97,A98;
then |.setopfunc(Y2, the carrier of X, REAL, L, addreal).| < e/2
by A87,XXREAL_0:2;
then |.setopfunc(Y0, the carrier of X, REAL, L, addreal) - r.| +
|.setopfunc(Y2, the carrier of X, REAL, L, addreal).| < e/2 + e/2 by A92,
XREAL_1:8;
hence |.r - setopfunc(Y1, the carrier of X, REAL, L, addreal).| <
e by A100,XXREAL_0:2;
end;
end;
hence |.r - setopfunc(Y1, the carrier of X, REAL, L, addreal).| < e;
end;
hence thesis by A89,A90;
end;
hence thesis;
end;
hence thesis by BHSP_6:def 6;
end;
theorem Th2:
for X st the addF of X is commutative associative & the addF of X
is having_a_unity for S be finite OrthogonalFamily of X st S is non empty for I
be Function of the carrier of X, the carrier of X st S c= dom I & (for y st y
in S holds I.y = y) for H be Function of the carrier of X, REAL st S c= dom H &
(for y st y in S holds H.y= (y.|.y)) holds setopfunc(S, the carrier of X, the
carrier of X, I, the addF of X) .|. setopfunc(S, the carrier of X, the carrier
of X, I, the addF of X) = setopfunc(S, the carrier of X, REAL, H, addreal)
proof
let X such that
A1: the addF of X is commutative associative & the addF of X is having_a_unity;
let S be finite OrthogonalFamily of X such that
A2: S is non empty;
let I be Function of the carrier of X, the carrier of X such that
A3: S c= dom I and
A4: for y st y in S holds I.y = y;
consider p be FinSequence of the carrier of X such that
A5: p is one-to-one & rng p = S and
A6: setopfunc(S, (the carrier of X), (the carrier of X), I, (the addF of
X)) = (the addF of X) "**" Func_Seq(I, p) by A1,BHSP_5:def 5;
let H be Function of the carrier of X, REAL such that
A7: S c= dom H and
A8: for y st y in S holds H.y= y.|.y;
A9: setopfunc(S, the carrier of X, REAL, H, addreal) = addreal "**" Func_Seq
(H, p) by A5,BHSP_5:def 5;
A10: for y1, y2 st y1 in S & y2 in S & y1 <> y2 holds (the scalar of X).[I.
y1, I.y2] = 0
proof
let y1, y2;
assume that
A11: y1 in S & y2 in S and
A12: y1 <> y2;
A13: y1.|.y2 = 0 by A11,A12,BHSP_5:def 8;
I.y1 = y1 & I.y2 = y2 by A4,A11;
hence thesis by A13,BHSP_1:def 1;
end;
for y st y in S holds H.y = (the scalar of X).[I.y, I.y]
proof
let y;
assume
A14: y in S;
then
A15: I.y = y by A4;
H.y = (y.|.y) by A8,A14
.= (the scalar of X).[I.y, I.y] by A15,BHSP_1:def 1;
hence thesis;
end;
then
(the scalar of X).[(the addF of X) "**" Func_Seq(I, p), (the addF of X)
"**" Func_Seq(I, p)] = addreal "**" Func_Seq(H, p) by A2,A3,A7,A5,A10,
BHSP_5:9;
hence thesis by A6,A9,BHSP_1:def 1;
end;
theorem Th3:
for X st the addF of X is commutative associative & the addF of X
is having_a_unity for S be finite OrthogonalFamily of X st S is non empty for H
be Functional of X st S c= dom H & (for x st x in S holds H.x = (x.|.x)) holds
(setsum(S)).|.(setsum(S)) = setopfunc(S, the carrier of X, REAL, H, addreal)
proof
let X such that
A1: the addF of X is commutative associative & the addF of X is having_a_unity;
reconsider I = id the carrier of X as Function of the carrier of X, the
carrier of X;
let S be finite OrthogonalFamily of X such that
A2: S is non empty;
let H be Functional of X such that
A3: S c= dom H & for x st x in S holds H.x = (x.|.x);
A4: for x st x in S holds I.x = x;
A5: dom I = the carrier of X by FUNCT_2:def 1;
for x be set st x in the carrier of X holds I.x = x by FUNCT_1:18;
then
setsum(S) = setopfunc(S, the carrier of X, the carrier of X, I, the addF
of X) by A1,A5,BHSP_6:1;
hence thesis by A1,A2,A3,A5,A4,Th2;
end;
theorem Th4:
for Y be OrthogonalFamily of X for Z be Subset of X holds Z is
Subset of Y implies Z is OrthogonalFamily of X
proof
let Y be OrthogonalFamily of X;
let Z be Subset of X;
assume Z is Subset of Y;
then for x, y st x in Z & y in Z & x <> y holds x.|.y = 0 by BHSP_5:def 8;
hence thesis by BHSP_5:def 8;
end;
theorem Th5:
for Y be OrthonormalFamily of X for Z be Subset of X holds Z is
Subset of Y implies Z is OrthonormalFamily of X
proof
let Y be OrthonormalFamily of X;
let Z be Subset of X;
assume
A1: Z is Subset of Y;
then
A2: for x st x in Z holds x.|.x = 1 by BHSP_5:def 9;
Y is OrthogonalFamily of X by BHSP_5:def 9;
then Z is OrthogonalFamily of X by A1,Th4;
hence thesis by A2,BHSP_5:def 9;
end;
begin :: Equivalence of summability
theorem Th6:
for X being RealHilbertSpace
st the addF of X is commutative associative & the addF of X
is having_a_unity for S be OrthonormalFamily of X for H be
Functional of X st S c= dom H &
(for x being Point of X st x in S holds H.x = (x.|.x)) holds S
is summable_set iff S is_summable_set_by H
proof
let X be RealHilbertSpace such that
A1: the addF of X is commutative associative & the addF of X is having_a_unity;
let S be OrthonormalFamily of X;
let H be Functional of X such that
A2: S c= dom H and
A3: for x being Point of X st x in S holds H.x = (x.|.x);
A4: now
assume
A5: S is summable_set;
now
let e be Real such that
A6: 0 < e;
set e9 = sqrt e;
0 < e9 by A6,SQUARE_1:25;
then consider e1 be Element of REAL such that
A7: 0 < e1 and
A8: e1 < e9 by CHAIN_1:1;
e1^2 < e9^2 by A7,A8,SQUARE_1:16;
then
A9: e1*e1 < e by A6,SQUARE_1:def 2;
consider Y0 be finite Subset of X such that
A10: Y0 is non empty & Y0 c= S and
A11: for Y1 be finite Subset of X st Y1 is non empty & Y1 c= S & Y0
misses Y1 holds ||.setsum(Y1).|| < e1 by A1,A5,A7,BHSP_6:10;
take Y0;
thus Y0 is non empty & Y0 c= S by A10;
let Y1 be finite Subset of X such that
A12: Y1 is non empty and
A13: Y1 c= S and
A14: Y0 misses Y1;
Y1 is finite OrthonormalFamily of X by A13,Th5;
then
A15: Y1 is finite OrthogonalFamily of X by BHSP_5:def 9;
for x being Point of X st x in Y1 holds H.x = (x.|.x) by A3,A13;
then
A16: (setsum(Y1)).|.(setsum(Y1)) = setopfunc(Y1, the carrier of X, REAL,
H, addreal) by A1,A2,A12,A13,A15,Th3,XBOOLE_1:1;
0 <= ||.setsum(Y1).|| by BHSP_1:28;
then ||.setsum(Y1).||^2 < e1^2 by A11,A12,A13,A14,SQUARE_1:16;
then
A17: ||.setsum(Y1).||^2 < e by A9,XXREAL_0:2;
||.setsum(Y1).|| = sqrt ((setsum(Y1)).|.(setsum(Y1))) & 0 <= (
setsum(Y1)).|. (setsum(Y1)) by BHSP_1:def 2,def 4;
then
A18: ||.setsum(Y1).||^2 = setopfunc(Y1, the carrier of X, REAL, H,
addreal) by A16,SQUARE_1:def 2;
0 <= setopfunc(Y1, the carrier of X, REAL, H, addreal) by A16,
BHSP_1:def 2;
hence |.setopfunc(Y1, the carrier of X, REAL, H, addreal).| < e by A17
,A18,ABSVALUE:def 1;
end;
hence S is_summable_set_by H by Th1;
end;
now
assume
A19: S is_summable_set_by H;
now
let e be Real such that
A20: 0 < e;
set e1 = e * e;
0 < e1 by A20,XREAL_1:129;
then consider Y0 be finite Subset of X such that
A21: Y0 is non empty & Y0 c= S and
A22: for Y1 be finite Subset of X st Y1 is non empty & Y1 c= S & Y0
misses Y1 holds |.setopfunc(Y1, the carrier of X, REAL, H, addreal).| < e1 by
A19,Th1;
now
let Y1 be finite Subset of X such that
A23: Y1 is non empty and
A24: Y1 c= S and
A25: Y0 misses Y1;
set F = setopfunc(Y1, the carrier of X, REAL, H, addreal);
Y1 is finite OrthonormalFamily of X by A24,Th5;
then
A26: Y1 is finite OrthogonalFamily of X by BHSP_5:def 9;
|.F.| < e1 by A22,A23,A24,A25;
then F - e1 < |.F.| - |.F.| by ABSVALUE:4,XREAL_1:15;
then
A27: F < e1 by XREAL_1:48;
for x being Point of X st x in Y1 holds H.x= (x.|.x) by A3,A24;
then
A28: (setsum Y1).|.(setsum Y1) = F by A1,A2,A23,A24,A26,Th3,XBOOLE_1:1;
0 <= (setsum Y1).|.(setsum Y1) & ||.setsum Y1.|| = sqrt ((setsum
Y1).|.( setsum Y1)) by BHSP_1:def 2,def 4;
then ||.setsum Y1.||^2 < e1 by A27,A28,SQUARE_1:def 2;
then sqrt(||.setsum(Y1).||^2) < sqrt(e^2) by SQUARE_1:27,XREAL_1:63;
then sqrt(||.setsum(Y1).||^2) < e by A20,SQUARE_1:22;
hence ||.setsum(Y1).|| < e by BHSP_1:28,SQUARE_1:22;
end;
hence ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= S & for Y1
be finite Subset of X st Y1 is non empty & Y1 c= S & Y0 misses Y1 holds ||.
setsum(Y1).|| < e by A21;
end;
hence S is summable_set by A1,BHSP_6:10;
end;
hence thesis by A4;
end;
theorem Th7:
for S be Subset of X st S is summable_set
for e be Real st
0 < e ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= S & for Y1 be
finite Subset of X st Y0 c= Y1 & Y1 c= S holds |.((sum(S)).|.(sum(S))) - ((
setsum(Y1)).|.(setsum(Y1))).| < e
proof
let S be Subset of X such that
A1: S is summable_set;
consider Y02 be finite Subset of X such that
Y02 is non empty and
A2: Y02 c= S and
A3: for Y1 be finite Subset of X st Y02 c= Y1 & Y1 c= S holds ||.sum(S)
- setsum(Y1).|| < 1 by A1,BHSP_6:def 3;
let e be Real such that
A4: 0 < e;
set e9 = e/(2*||.sum(S).||+1);
0 <= ||.sum(S).|| by BHSP_1:28;
then 0 <= 2*||.sum(S).||;
then
A5: 0+0 < 2*||.sum(S).||+1;
then 0 < e9 by A4,XREAL_1:139;
then consider Y01 be finite Subset of X such that
A6: Y01 is non empty and
A7: Y01 c= S and
A8: for Y1 be finite Subset of X st Y01 c= Y1 & Y1 c= S holds ||.sum(S)
- setsum(Y1).|| < e9 by A1,BHSP_6:def 3;
set Y0 = Y01 \/ Y02;
A9: for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= S holds |.((sum(S))
.|.(sum(S))) - ((setsum(Y1)).|.(setsum(Y1))).| < e
proof
let Y1 be finite Subset of X such that
A10: Y0 c= Y1 and
A11: Y1 c= S;
set SS = sum(S)-setsum(Y1), SY = setsum(Y1);
Y01 c= Y1 by A10,XBOOLE_1:11;
then
A12: ||.SS.||*(2*||.sum(S).|| + 1) < e9*(2*||.sum(S).|| + 1) by A5,A8,A11,
XREAL_1:68;
||.SY.|| = ||.-SY.|| by BHSP_1:31
.= ||.0.X - SY.|| by RLVECT_1:14
.= ||.-sum(S) + sum(S) - SY.|| by RLVECT_1:5
.= ||.-sum(S) + SS.|| by RLVECT_1:def 3;
then ||.SY.|| <= ||.-sum(S).|| + ||.SS.|| by BHSP_1:30;
then
A13: ||.SY.|| <= ||.sum(S).|| + ||.SS.|| by BHSP_1:31;
Y02 c= Y1 by A10,XBOOLE_1:11;
then ||.SS.|| + ||.SY.|| < 1 + (||.sum(S).|| + ||.SS.||) by A3,A11,A13,
XREAL_1:8;
then ||.SY.|| + ||.SS.|| - ||.SS.|| < 1 + ||.sum(S).|| + ||.SS.|| - ||.SS
.|| by XREAL_1:14;
then
A14: ||.sum(S).|| + ||.SY.|| < 1 + ||.sum(S).|| + ||.sum(S).|| by XREAL_1:8;
0 <= ||.SS.|| by BHSP_1:28;
then ||.SS.||*(||.sum(S).|| + ||.SY.||) <= ||.SS.||*(2*||.sum(S).|| + 1)
by A14,XREAL_1:64;
then ||.SS.||*(||.sum(S).|| + ||.SY.||) + ||.SS.||*(2*||.sum(S).|| + 1) <
e9*(2*||.sum(S).|| + 1) + ||.SS.||*(2*||.sum(S).|| + 1) by A12,XREAL_1:8;
then ||.SS.||*(||.sum(S).|| + ||.SY.||) + ||.SS.||*(2*||.sum(S).|| + 1) -
||.SS.||*(2*||.sum(S).|| + 1) < e9*(2*||.sum(S).|| + 1) + ||.SS.||*(2*||.sum(S)
.|| + 1) - ||.SS.||*(2*||.sum(S).|| + 1) by XREAL_1:14;
then
A15: ||.SS.||*(||.sum(S).|| + ||.SY.||) < e by A5,XCMPLX_1:87;
set F = (sum(S)).|.(sum(S)), G = (setsum(Y1)).|.(setsum(Y1));
|.F - G.| = |.F - ((sum(S)).|.SY) + (((sum(S)).|.SY) - G).|
.= |.((sum(S)).|.SS) + (((sum(S)).|.SY) - G).| by BHSP_1:12
.= |.((sum(S)).|.SS) + (SS.|.SY).| by BHSP_1:11;
then
A16: |.F - G.| <= |.((sum(S)).|.SS).| + |.SS.|.SY.| by COMPLEX1:56;
|.((sum(S)).|.SS).| <= ||.sum(S).||*||.SS.|| by BHSP_1:29;
then
|.F - G.| + |.((sum(S)).|.SS).| <= |.((sum(S)).|.SS).| + |.SS.|.
SY.| + ||.sum(S).||*||.SS.|| by A16,XREAL_1:7;
then
|.F - G.| + |.((sum(S)).|.SS).| <= (|.SS.|.SY.| + ||.sum(S).||*||.
SS.||) + |.((sum(S)).|.SS).|;
then
A17: |.F - G.| <= |.SS.|.SY.| + ||.sum(S).||*||.SS.|| by XREAL_1:6;
|.SS.|.SY.| <= ||.SS.||*||.SY.|| by BHSP_1:29;
then |.F - G.| + |.SS.|.SY.| <= |.SS.|.SY.| + ||.sum(S).||*||.SS.|| +
||.SS.||*||.SY.|| by A17,XREAL_1:7;
then |.F - G.| + |.SS.|.SY.| <= ||.sum(S).||*||.SS.|| + ||.SS.||*||.SY
.|| + |.SS.|.SY.|;
then |.F - G.| <= ||.SS.||*||.sum(S).|| + ||.SS.||*||.SY.|| by XREAL_1:6;
then |.F - G.| + ||.SS.||*(||.sum(S).|| + ||.SY.||) < e + ||.SS.||*(||.
sum(S).|| + ||.SY.||) by A15,XREAL_1:8;
then
|.F - G.| + ||.SS.||*(||.sum(S).|| + ||.SY.||) - ||.SS.||*(||.sum(S)
.|| + ||.SY.||) < e + ||.SS.||*(||.sum(S).|| + ||.SY.||) - ||.SS.||*(||.sum(S)
.|| + ||.SY.||) by XREAL_1:14;
hence thesis;
end;
Y0 c= S by A7,A2,XBOOLE_1:8;
hence thesis by A6,A9;
end;
Lm4: for p1, p2 being Real st
for e be Real st 0 < e holds |.p1 - p2.|
< e holds p1 = p2
proof
let p1, p2 be Real;
assume
A1: for e be Real st 0 < e holds |.p1 - p2.| < e;
assume p1 <> p2;
then p1 - p2 <> 0;
then 0 < |.p1-p2.| by COMPLEX1:47;
hence contradiction by A1;
end;
theorem
for X being RealHilbertSpace
st the addF of X is commutative associative & the addF of X is
having_a_unity for S be OrthonormalFamily of X for H be
Functional of X st S c= dom H &
(for x being Point of X st x in S holds H.x = (x.|.x)) holds S
is summable_set implies (sum(S)).|.(sum(S)) = sum_byfunc(S, H)
proof
let X be RealHilbertSpace such that
A1: the addF of X is commutative associative & the addF of X is having_a_unity;
let S be OrthonormalFamily of X;
let H be Functional of X such that
A2: S c= dom H and
A3: for x being Point of X st x in S holds H.x= (x.|.x);
A4: for Y1 be finite Subset of X st Y1 is non empty & Y1 c= S holds (setsum(
Y1)).|.(setsum(Y1)) = setopfunc(Y1, the carrier of X, REAL, H,addreal)
proof
let Y1 be finite Subset of X such that
A5: Y1 is non empty and
A6: Y1 c= S;
Y1 is finite OrthonormalFamily of X by A6,Th5;
then
A7: Y1 is finite OrthogonalFamily of X by BHSP_5:def 9;
for x being Point of X st x in Y1 holds H.x = (x.|.x) by A3,A6;
hence thesis by A1,A2,A5,A6,A7,Th3,XBOOLE_1:1;
end;
set p1 = (sum(S)).|.(sum(S)), p2 = sum_byfunc(S, H);
assume
A8: S is summable_set;
then
A9: S is_summable_set_by H by A1,A2,A3,Th6;
for e be Real st 0 < e holds |.p1 - p2.| < e
proof
let e be Real;
assume 0 < e;
then
A10: 0/2 < e/2 by XREAL_1:74;
then consider Y02 be finite Subset of X such that
Y02 is non empty and
A11: Y02 c= S and
A12: for Y1 be finite Subset of X st Y02 c= Y1 & Y1 c= S holds |.p2
- setopfunc(Y1, the carrier of X, REAL, H, addreal).| < e/2 by A9,BHSP_6:def 7;
consider Y01 be finite Subset of X such that
A13: Y01 is non empty and
A14: Y01 c= S and
A15: for Y1 be finite Subset of X st Y01 c= Y1 & Y1 c= S holds |.p1
- ((setsum Y1).|.(setsum Y1)).| < e/2 by A8,A10,Th7;
set Y1 = Y01 \/ Y02;
A16: Y1 c= S by A14,A11,XBOOLE_1:8;
reconsider Y011 = Y01 as non empty set by A13;
set r = setopfunc(Y1, the carrier of X, REAL, H, addreal);
Y1 = Y011 \/ Y02;
then (setsum(Y1)).|.(setsum(Y1)) = r by A4,A14,A11,XBOOLE_1:8;
then Y02 c= Y1 & |.p1 - r.| < e/2 by A15,A16,XBOOLE_1:7;
then |.p1-r.| + |.p2-r.| < e/2 + e/2 by A12,A16,XREAL_1:8;
then
A17: |.p1-r.| + |.r-p2.| < e by UNIFORM1:11;
p1 - p2 = (p1 - r) + (r - p2);
then |.p1-p2.| <= |.p1-r.| + |.r-p2.| by COMPLEX1:56;
hence thesis by A17,XXREAL_0:2;
end;
hence thesis by Lm4;
end;