let X be RealUnitarySpace; :: thesis: for Y being Subset of X

for L being Functional of X holds

( Y is_summable_set_by L iff for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) )

let Y be Subset of X; :: thesis: for L being Functional of X holds

( Y is_summable_set_by L iff for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) )

let L be Functional of X; :: thesis: ( Y is_summable_set_by L iff for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) )

thus ( Y is_summable_set_by L implies for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) ) :: thesis: ( ( for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) ) implies Y is_summable_set_by L )

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) ; :: thesis: Y is_summable_set_by L

ex r being Real st

for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )

for L being Functional of X holds

( Y is_summable_set_by L iff for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) )

let Y be Subset of X; :: thesis: for L being Functional of X holds

( Y is_summable_set_by L iff for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) )

let L be Functional of X; :: thesis: ( Y is_summable_set_by L iff for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) )

thus ( Y is_summable_set_by L implies for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) ) :: thesis: ( ( for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) ) implies Y is_summable_set_by L )

proof

assume A9:
for e being Real st 0 < e holds
assume
Y is_summable_set_by L
; :: thesis: for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) )

then consider r being Real such that

A1: for e being Real st e > 0 holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being 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 being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) )

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) ; :: thesis: verum

end;ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) )

then consider r being Real such that

A1: for e being Real st e > 0 holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being 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 being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) )

proof

hence
for e being Real st 0 < e holds
let e be Real; :: thesis: ( 0 < e implies ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) )

assume 0 < e ; :: thesis: ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) )

then consider Y0 being finite Subset of X such that

A2: not Y0 is empty and

A3: Y0 c= Y and

A4: for Y1 being 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 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) by A2, A3; :: thesis: verum

end;( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) )

assume 0 < e ; :: thesis: ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) )

then consider Y0 being finite Subset of X such that

A2: not Y0 is empty and

A3: Y0 c= Y and

A4: for Y1 being 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 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e

proof

hence
ex Y0 being finite Subset of X st
let Y1 be finite Subset of X; :: thesis: ( not Y1 is empty & Y1 c= Y & Y0 misses Y1 implies |.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e )

assume that

not Y1 is empty and

A5: Y1 c= Y and

A6: Y0 misses Y1 ; :: thesis: |.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e

set Y19 = Y0 \/ Y1;

dom L = the carrier of X by FUNCT_2:def 1;

then setopfunc ((Y0 \/ Y1), 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 ((Y0 \/ Y1), the carrier of X,REAL,L,addreal)) - (setopfunc (Y0, the carrier of X,REAL,L,addreal)) ;

Y0 c= Y0 \/ Y1 by XBOOLE_1:7;

then |.(r - (setopfunc ((Y0 \/ Y1), the carrier of X,REAL,L,addreal))).| < e / 2 by A3, A4, A5, XBOOLE_1:8;

then A8: |.((setopfunc ((Y0 \/ Y1), 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 |.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e by A8, A7, Lm1; :: thesis: verum

end;assume that

not Y1 is empty and

A5: Y1 c= Y and

A6: Y0 misses Y1 ; :: thesis: |.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e

set Y19 = Y0 \/ Y1;

dom L = the carrier of X by FUNCT_2:def 1;

then setopfunc ((Y0 \/ Y1), 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 ((Y0 \/ Y1), the carrier of X,REAL,L,addreal)) - (setopfunc (Y0, the carrier of X,REAL,L,addreal)) ;

Y0 c= Y0 \/ Y1 by XBOOLE_1:7;

then |.(r - (setopfunc ((Y0 \/ Y1), the carrier of X,REAL,L,addreal))).| < e / 2 by A3, A4, A5, XBOOLE_1:8;

then A8: |.((setopfunc ((Y0 \/ Y1), 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 |.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e by A8, A7, Lm1; :: thesis: verum

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) by A2, A3; :: thesis: verum

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) ; :: thesis: verum

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) ; :: thesis: Y is_summable_set_by L

ex r being Real st

for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )

proof

hence
Y is_summable_set_by L
by BHSP_6:def 6; :: thesis: verum
defpred S_{1}[ object , object ] means ex D2 being set st

( D2 = $2 & $2 is finite Subset of X & not D2 is empty & D2 c= Y & ( for z being Real st z = $1 holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & D2 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) );

A10: for x being object st x in NAT holds

ex y being object st

( y in bool Y & S_{1}[x,y] )

for x being object st x in NAT holds

S_{1}[x,B . x]
from FUNCT_2:sch 1(A10);

ex A being sequence of (bool Y) st

for i being Nat holds

( A . i is finite Subset of X & not A . i is empty & A . i c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . i misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds

A . i c= A . j ) )

A40: for i being Nat holds

( A . i is finite Subset of X & not A . i is empty & A . i c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . i misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds

A . i c= A . j ) ) ;

defpred S_{2}[ object , object ] means ex Y1 being finite Subset of X st

( not Y1 is empty & A . $1 = Y1 & $2 = setopfunc (Y1, the carrier of X,REAL,L,addreal) );

A41: for x being object st x in NAT holds

ex y being object st

( y in REAL & S_{2}[x,y] )

for x being object st x in NAT holds

S_{2}[x,F . x]
from FUNCT_2:sch 1(A41);

then consider F being sequence of REAL such that

A42: for x being object st x in NAT holds

ex Y1 being finite Subset of X st

( not Y1 is empty & A . x = Y1 & F . x = setopfunc (Y1, the carrier of X,REAL,L,addreal) ) ;

set seq = F;

A43: for e being Real st e > 0 holds

ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

|.((F . n) - (F . m)).| < e

ex k being Nat st

for m being Nat st k <= m holds

|.((F . m) - (F . k)).| < e

then consider x being Real such that

A84: for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

|.((F . n) - x).| < r by SEQ_2:def 6;

reconsider r = x as Real ;

take r ; :: thesis: for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )

for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) ; :: thesis: verum

end;( D2 = $2 & $2 is finite Subset of X & not D2 is empty & D2 c= Y & ( for z being Real st z = $1 holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & D2 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) );

A10: for x being object st x in NAT holds

ex y being object st

( y in bool Y & S

proof

A13:
ex B being sequence of (bool Y) st
let x be object ; :: thesis: ( x in NAT implies ex y being object st

( y in bool Y & S_{1}[x,y] ) )

assume x in NAT ; :: thesis: ex y being object st

( y in bool Y & S_{1}[x,y] )

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 being finite Subset of X such that

A11: not Y0 is empty and

A12: ( Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) by A9;

take Y0 ; :: thesis: ( Y0 in bool Y & S_{1}[x,Y0] )

thus Y0 in bool Y by A12, ZFMISC_1:def 1; :: thesis: S_{1}[x,Y0]

take D2 = Y0; :: thesis: ( D2 = Y0 & Y0 is finite Subset of X & not D2 is empty & D2 c= Y & ( for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & D2 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) )

thus D2 = Y0 ; :: thesis: ( Y0 is finite Subset of X & not D2 is empty & D2 c= Y & ( for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & D2 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) )

thus Y0 is finite Subset of X ; :: thesis: ( not D2 is empty & D2 c= Y & ( for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & D2 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) )

thus not D2 is empty by A11; :: thesis: ( D2 c= Y & ( for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & D2 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) )

thus D2 c= Y by A12; :: thesis: for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & D2 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1)

for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is 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 being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & D2 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ; :: thesis: verum

end;( y in bool Y & S

assume x in NAT ; :: thesis: ex y being object st

( y in bool Y & S

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 being finite Subset of X such that

A11: not Y0 is empty and

A12: ( Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) by A9;

take Y0 ; :: thesis: ( Y0 in bool Y & S

thus Y0 in bool Y by A12, ZFMISC_1:def 1; :: thesis: S

take D2 = Y0; :: thesis: ( D2 = Y0 & Y0 is finite Subset of X & not D2 is empty & D2 c= Y & ( for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & D2 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) )

thus D2 = Y0 ; :: thesis: ( Y0 is finite Subset of X & not D2 is empty & D2 c= Y & ( for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & D2 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) )

thus Y0 is finite Subset of X ; :: thesis: ( not D2 is empty & D2 c= Y & ( for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & D2 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) )

thus not D2 is empty by A11; :: thesis: ( D2 c= Y & ( for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & D2 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) )

thus D2 c= Y by A12; :: thesis: for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & D2 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1)

for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is 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 being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & D2 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ; :: thesis: verum

for x being object st x in NAT holds

S

ex A being sequence of (bool Y) st

for i being Nat holds

( A . i is finite Subset of X & not A . i is empty & A . i c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . i misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds

A . i c= A . j ) )

proof

then consider A being sequence of (bool Y) such that
consider B being sequence of (bool Y) such that

A14: for x being object st x in NAT holds

S_{1}[x,B . x]
by A13;

A15: for x being object st x in NAT holds

( B . x is finite Subset of X & not B . x is empty & B . x c= Y & ( for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & B . x misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) )_{1}( Nat, set ) -> 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) = H_{1}(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 S_{2}[ Nat] means ( A . $1 is finite Subset of X & not A . $1 is empty & A . $1 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . $1 misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / ($1 + 1) ) & ( for j being Element of NAT st $1 <= j holds

A . $1 c= A . j ) );

for j being Nat st j0 <= j holds

A . j0 c= A . j_{2}[ 0 ]
by A15, A18;

A37: for i being Nat holds S_{2}[i]
from NAT_1:sch 2(A36, A20);

rng A c= bool Y

hence ex A being sequence of (bool Y) st

for i being Nat holds

( A . i is finite Subset of X & not A . i is empty & A . i c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . i misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds

A . i c= A . j ) ) by A37; :: thesis: verum

end;A14: for x being object st x in NAT holds

S

A15: for x being object st x in NAT holds

( B . x is finite Subset of X & not B . x is empty & B . x c= Y & ( for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & B . x misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) )

proof

deffunc H
let x be object ; :: thesis: ( x in NAT implies ( B . x is finite Subset of X & not B . x is empty & B . x c= Y & ( for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & B . x misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) ) )

assume A16: x in NAT ; :: thesis: ( B . x is finite Subset of X & not B . x is empty & B . x c= Y & ( for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & B . x misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) )

S_{1}[x,B . x]
by A16, A14;

hence ( B . x is finite Subset of X & not B . x is empty & B . x c= Y & ( for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & B . x misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) ) ; :: thesis: verum

end;for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & B . x misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) ) )

assume A16: x in NAT ; :: thesis: ( B . x is finite Subset of X & not B . x is empty & B . x c= Y & ( for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & B . x misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) )

S

hence ( B . x is finite Subset of X & not B . x is empty & B . x c= Y & ( for z being Real st z = x holds

for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & B . x misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) ) ; :: thesis: verum

ex A being Function st

( dom A = NAT & A . 0 = B . 0 & ( for n being Nat holds A . (n + 1) = H

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 S

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / ($1 + 1) ) & ( for j being Element of NAT st $1 <= j holds

A . $1 c= A . j ) );

A20: now :: thesis: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]

for j0 being Nat st j0 = 0 holds S

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

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

A22: for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . (n + 1) misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / ((n + 1) + 1)_{3}[ Nat] means ( n + 1 <= $1 implies A . (n + 1) c= A . $1 );

A25: for j being Nat st S_{3}[j] holds

S_{3}[j + 1]
_{3}[ 0 ]
;

A31: for j being Nat holds S_{3}[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 S_{2}[n + 1]
by A21, A22, A31, XBOOLE_1:8; :: thesis: verum

end;assume A21: S

A22: for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . (n + 1) misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / ((n + 1) + 1)

proof

defpred S
let Y1 be finite Subset of X; :: thesis: ( not Y1 is empty & Y1 c= Y & A . (n + 1) misses Y1 implies |.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / ((n + 1) + 1) )

assume that

A23: ( not Y1 is empty & Y1 c= Y ) and

A24: A . (n + 1) misses Y1 ; :: thesis: |.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / ((n + 1) + 1)

A . (n + 1) = (B . (n + 1)) \/ (A . n) by A19;

then B . (n + 1) misses Y1 by A24, XBOOLE_1:7, XBOOLE_1:63;

hence |.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / ((n + 1) + 1) by A15, A23; :: thesis: verum

end;assume that

A23: ( not Y1 is empty & Y1 c= Y ) and

A24: A . (n + 1) misses Y1 ; :: thesis: |.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / ((n + 1) + 1)

A . (n + 1) = (B . (n + 1)) \/ (A . n) by A19;

then B . (n + 1) misses Y1 by A24, XBOOLE_1:7, XBOOLE_1:63;

hence |.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / ((n + 1) + 1) by A15, A23; :: thesis: verum

A25: for j being Nat st S

S

proof

A30:
S
let j be Nat; :: thesis: ( S_{3}[j] implies S_{3}[j + 1] )

assume that

A26: S_{3}[j]
and

A27: n + 1 <= j + 1 ; :: thesis: A . (n + 1) c= A . (j + 1)

end;assume that

A26: S

A27: n + 1 <= j + 1 ; :: thesis: A . (n + 1) c= A . (j + 1)

now :: thesis: ( ( n = j & A . (n + 1) c= A . (j + 1) ) or ( n <> j & A . (n + 1) c= A . (j + 1) ) )end;

hence
A . (n + 1) c= A . (j + 1)
; :: thesis: verumA31: for j being Nat holds S

( A . (n + 1) = (B . (n + 1)) \/ (A . n) & B . (n + 1) is finite Subset of X ) by A15, A19;

hence S

for j being Nat st j0 <= j holds

A . j0 c= A . j

proof

then A36:
S
let j0 be Nat; :: thesis: ( j0 = 0 implies for j being Nat st j0 <= j holds

A . j0 c= A . j )

assume A32: j0 = 0 ; :: thesis: for j being Nat st j0 <= j holds

A . j0 c= A . j

defpred S_{3}[ Nat] means ( j0 <= $1 implies A . j0 c= A . $1 );

_{3}[ 0 ]
by A32;

thus for j being Nat holds S_{3}[j]
from NAT_1:sch 2(A35, A33); :: thesis: verum

end;A . j0 c= A . j )

assume A32: j0 = 0 ; :: thesis: for j being Nat st j0 <= j holds

A . j0 c= A . j

defpred S

A33: now :: thesis: for j being Nat st S_{3}[j] holds

S_{3}[j + 1]

A35:
SS

let j be Nat; :: thesis: ( S_{3}[j] implies S_{3}[j + 1] )

assume A34: S_{3}[j]
; :: thesis: S_{3}[j + 1]

A . (j + 1) = (B . (j + 1)) \/ (A . j) by A19;

then A . j c= A . (j + 1) by XBOOLE_1:7;

hence S_{3}[j + 1]
by A32, A34, XBOOLE_1:1; :: thesis: verum

end;assume A34: S

A . (j + 1) = (B . (j + 1)) \/ (A . j) by A19;

then A . j c= A . (j + 1) by XBOOLE_1:7;

hence S

thus for j being Nat holds S

A37: for i being Nat holds S

rng A c= bool Y

proof

then
A is sequence of (bool Y)
by A17, FUNCT_2:2;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng A or y in bool Y )

assume y in rng A ; :: thesis: y in bool Y

then consider x being 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 y in bool Y by A39, ZFMISC_1:def 1; :: thesis: verum

end;assume y in rng A ; :: thesis: y in bool Y

then consider x being 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 y in bool Y by A39, ZFMISC_1:def 1; :: thesis: verum

hence ex A being sequence of (bool Y) st

for i being Nat holds

( A . i is finite Subset of X & not A . i is empty & A . i c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . i misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds

A . i c= A . j ) ) by A37; :: thesis: verum

A40: for i being Nat holds

( A . i is finite Subset of X & not A . i is empty & A . i c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . i misses Y1 holds

|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds

A . i c= A . j ) ) ;

defpred S

( not Y1 is empty & A . $1 = Y1 & $2 = setopfunc (Y1, the carrier of X,REAL,L,addreal) );

A41: for x being object st x in NAT holds

ex y being object st

( y in REAL & S

proof

ex F being sequence of REAL st
let x be object ; :: thesis: ( x in NAT implies ex y being object st

( y in REAL & S_{2}[x,y] ) )

assume x in NAT ; :: thesis: ex y being object st

( y in REAL & S_{2}[x,y] )

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 ;

not A . i is empty by A40;

then ex Y1 being finite Subset of X st

( not Y1 is empty & A . x = Y1 & y = setopfunc (Y1, the carrier of X,REAL,L,addreal) ) ;

hence ex y being object st

( y in REAL & S_{2}[x,y] )
; :: thesis: verum

end;( y in REAL & S

assume x in NAT ; :: thesis: ex y being object st

( y in REAL & S

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 ;

not A . i is empty by A40;

then ex Y1 being finite Subset of X st

( not Y1 is empty & A . x = Y1 & y = setopfunc (Y1, the carrier of X,REAL,L,addreal) ) ;

hence ex y being object st

( y in REAL & S

for x being object st x in NAT holds

S

then consider F being sequence of REAL such that

A42: for x being object st x in NAT holds

ex Y1 being finite Subset of X st

( not Y1 is empty & A . x = Y1 & F . x = setopfunc (Y1, the carrier of X,REAL,L,addreal) ) ;

set seq = F;

A43: for e being Real st e > 0 holds

ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

|.((F . n) - (F . m)).| < e

proof

for e being Real st 0 < e holds
let e be Real; :: thesis: ( e > 0 implies ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

|.((F . n) - (F . m)).| < e )

assume A44: e > 0 ; :: thesis: ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

|.((F . n) - (F . m)).| < e

A45: e / 2 > 0 / 2 by A44, XREAL_1:74;

then consider k being Nat such that

A46: 1 / (k + 1) < e / 2 by Lm2;

take k ; :: thesis: for n, m being Nat st n >= k & m >= k holds

|.((F . n) - (F . m)).| < e

let nn, mm be Nat; :: thesis: ( nn >= k & mm >= k implies |.((F . nn) - (F . mm)).| < e )

assume that

A47: nn >= k and

A48: mm >= k ; :: thesis: |.((F . nn) - (F . mm)).| < e

reconsider m = mm, n = nn, k = k as Element of NAT by ORDINAL1:def 12;

consider Y2 being finite Subset of X such that

not Y2 is empty and

A49: A . m = Y2 and

A50: F . m = setopfunc (Y2, the carrier of X,REAL,L,addreal) by A42;

consider Y0 being finite Subset of X such that

not Y0 is empty and

A51: A . k = Y0 and

F . k = setopfunc (Y0, the carrier of X,REAL,L,addreal) by A42;

A52: Y0 c= Y2 by A40, A48, A51, A49;

consider Y1 being finite Subset of X such that

not Y1 is empty and

A53: A . n = Y1 and

A54: F . n = setopfunc (Y1, the carrier of X,REAL,L,addreal) by A42;

A55: Y0 c= Y1 by A40, A47, A51, A53;

end;for n, m being Nat st n >= k & m >= k holds

|.((F . n) - (F . m)).| < e )

assume A44: e > 0 ; :: thesis: ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

|.((F . n) - (F . m)).| < e

A45: e / 2 > 0 / 2 by A44, XREAL_1:74;

then consider k being Nat such that

A46: 1 / (k + 1) < e / 2 by Lm2;

take k ; :: thesis: for n, m being Nat st n >= k & m >= k holds

|.((F . n) - (F . m)).| < e

let nn, mm be Nat; :: thesis: ( nn >= k & mm >= k implies |.((F . nn) - (F . mm)).| < e )

assume that

A47: nn >= k and

A48: mm >= k ; :: thesis: |.((F . nn) - (F . mm)).| < e

reconsider m = mm, n = nn, k = k as Element of NAT by ORDINAL1:def 12;

consider Y2 being finite Subset of X such that

not Y2 is empty and

A49: A . m = Y2 and

A50: F . m = setopfunc (Y2, the carrier of X,REAL,L,addreal) by A42;

consider Y0 being finite Subset of X such that

not Y0 is empty and

A51: A . k = Y0 and

F . k = setopfunc (Y0, the carrier of X,REAL,L,addreal) by A42;

A52: Y0 c= Y2 by A40, A48, A51, A49;

consider Y1 being finite Subset of X such that

not Y1 is empty and

A53: A . n = Y1 and

A54: F . n = setopfunc (Y1, the carrier of X,REAL,L,addreal) by A42;

A55: Y0 c= Y1 by A40, A47, A51, A53;

now :: thesis: ( ( Y0 = Y1 & |.((F . nn) - (F . mm)).| < e ) or ( Y0 <> Y1 & |.((F . nn) - (F . mm)).| < e ) )end;

hence
|.((F . nn) - (F . mm)).| < e
; :: thesis: verumper cases
( Y0 = Y1 or Y0 <> Y1 )
;

end;

case A56:
Y0 = Y1
; :: thesis: |.((F . nn) - (F . mm)).| < e

end;

now :: thesis: ( ( Y0 = Y2 & |.((F . nn) - (F . mm)).| < e ) or ( Y0 <> Y2 & |.((F . nn) - (F . mm)).| < e ) )end;

hence
|.((F . nn) - (F . mm)).| < e
; :: thesis: verumper cases
( Y0 = Y2 or Y0 <> Y2 )
;

end;

case A57:
Y0 <> Y2
; :: thesis: |.((F . nn) - (F . mm)).| < e

ex Y02 being finite Subset of X st

( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )

A59: ( not Y02 is 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: |.((F . n) - (F . 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 |.((F . nn) - (F . mm)).| < e by A62, A63, XXREAL_0:2; :: thesis: verum

end;( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )

proof

then consider Y02 being finite Subset of X such that
take Y02 = Y2 \ Y0; :: thesis: ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )

A58: Y2 \ Y0 c= Y2 by XBOOLE_1:36;

Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39

.= Y2 by A52, XBOOLE_1:12 ;

hence ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A49, A57, A58, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

end;A58: Y2 \ Y0 c= Y2 by XBOOLE_1:36;

Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39

.= Y2 by A52, XBOOLE_1:12 ;

hence ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A49, A57, A58, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

A59: ( not Y02 is 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: |.((F . n) - (F . 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 |.((F . nn) - (F . mm)).| < e by A62, A63, XXREAL_0:2; :: thesis: verum

case A64:
Y0 <> Y1
; :: thesis: |.((F . nn) - (F . mm)).| < e

end;

now :: thesis: ( ( Y0 = Y2 & |.((F . nn) - (F . mm)).| < e ) or ( Y0 <> Y2 & |.((F . nn) - (F . mm)).| < e ) )end;

hence
|.((F . nn) - (F . mm)).| < e
; :: thesis: verumper cases
( Y0 = Y2 or Y0 <> Y2 )
;

end;

case A65:
Y0 = Y2
; :: thesis: |.((F . nn) - (F . mm)).| < e

ex Y01 being finite Subset of X st

( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )

A67: ( not Y01 is 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 |.((F . n) - (F . m)).| < e / 2 by A46, A54, A50, A65, A70, XXREAL_0:2;

then |.((F . n) - (F . m)).| + 0 < (e / 2) + (e / 2) by A45, XREAL_1:8;

hence |.((F . nn) - (F . mm)).| < e ; :: thesis: verum

end;( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )

proof

then consider Y01 being finite Subset of X such that
take Y01 = Y1 \ Y0; :: thesis: ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )

A66: Y1 \ Y0 c= Y1 by XBOOLE_1:36;

Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39

.= Y1 by A55, XBOOLE_1:12 ;

hence ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A53, A64, A66, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

end;A66: Y1 \ Y0 c= Y1 by XBOOLE_1:36;

Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39

.= Y1 by A55, XBOOLE_1:12 ;

hence ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A53, A64, A66, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

A67: ( not Y01 is 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 |.((F . n) - (F . m)).| < e / 2 by A46, A54, A50, A65, A70, XXREAL_0:2;

then |.((F . n) - (F . m)).| + 0 < (e / 2) + (e / 2) by A45, XREAL_1:8;

hence |.((F . nn) - (F . mm)).| < e ; :: thesis: verum

case A71:
Y0 <> Y2
; :: thesis: |.((F . nn) - (F . mm)).| < e

ex Y02 being finite Subset of X st

( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )

A73: ( not Y02 is 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 being finite Subset of X st

( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )

A78: ( not Y01 is 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 (F . n) - (F . 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: |.((F . n) - (F . 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 |.((F . nn) - (F . mm)).| < e by A81, XXREAL_0:2; :: thesis: verum

end;( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )

proof

then consider Y02 being finite Subset of X such that
take Y02 = Y2 \ Y0; :: thesis: ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )

A72: Y2 \ Y0 c= Y2 by XBOOLE_1:36;

Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39

.= Y2 by A52, XBOOLE_1:12 ;

hence ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A49, A71, A72, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

end;A72: Y2 \ Y0 c= Y2 by XBOOLE_1:36;

Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39

.= Y2 by A52, XBOOLE_1:12 ;

hence ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A49, A71, A72, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

A73: ( not Y02 is 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 being finite Subset of X st

( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )

proof

then consider Y01 being finite Subset of X such that
take Y01 = Y1 \ Y0; :: thesis: ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )

A77: Y1 \ Y0 c= Y1 by XBOOLE_1:36;

Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39

.= Y1 by A55, XBOOLE_1:12 ;

hence ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A53, A64, A77, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

end;A77: Y1 \ Y0 c= Y1 by XBOOLE_1:36;

Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39

.= Y1 by A55, XBOOLE_1:12 ;

hence ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A53, A64, A77, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

A78: ( not Y01 is 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 (F . n) - (F . 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: |.((F . n) - (F . 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 |.((F . nn) - (F . mm)).| < e by A81, XXREAL_0:2; :: thesis: verum

ex k being Nat st

for m being Nat st k <= m holds

|.((F . m) - (F . k)).| < e

proof

then
F is convergent
by SEQ_4:41;
let e be Real; :: thesis: ( 0 < e implies ex k being Nat st

for m being Nat st k <= m holds

|.((F . m) - (F . k)).| < e )

assume 0 < e ; :: thesis: ex k being Nat st

for m being Nat st k <= m holds

|.((F . m) - (F . k)).| < e

then consider k being Nat such that

A83: for n, m being Nat st n >= k & m >= k holds

|.((F . n) - (F . m)).| < e by A43;

for m being Nat st k <= m holds

|.((F . m) - (F . k)).| < e by A83;

hence ex k being Nat st

for m being Nat st k <= m holds

|.((F . m) - (F . k)).| < e ; :: thesis: verum

end;for m being Nat st k <= m holds

|.((F . m) - (F . k)).| < e )

assume 0 < e ; :: thesis: ex k being Nat st

for m being Nat st k <= m holds

|.((F . m) - (F . k)).| < e

then consider k being Nat such that

A83: for n, m being Nat st n >= k & m >= k holds

|.((F . n) - (F . m)).| < e by A43;

for m being Nat st k <= m holds

|.((F . m) - (F . k)).| < e by A83;

hence ex k being Nat st

for m being Nat st k <= m holds

|.((F . m) - (F . k)).| < e ; :: thesis: verum

then consider x being Real such that

A84: for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

|.((F . n) - x).| < r by SEQ_2:def 6;

reconsider r = x as Real ;

take r ; :: thesis: for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )

for e being Real st 0 < e holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )

proof

hence
for e being Real st 0 < e holds
let e be Real; :: thesis: ( 0 < e implies ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) )

assume e > 0 ; :: thesis: ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )

then A85: e / 2 > 0 / 2 by XREAL_1:74;

then consider m being Nat such that

A86: for n being Nat st n >= m holds

|.((F . n) - r).| < e / 2 by A84;

consider i being 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 being finite Subset of X such that

A89: not Y0 is empty and

A90: A . ii = Y0 and

A91: F . 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;

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) by A89, A90; :: thesis: verum

end;( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) )

assume e > 0 ; :: thesis: ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )

then A85: e / 2 > 0 / 2 by XREAL_1:74;

then consider m being Nat such that

A86: for n being Nat st n >= m holds

|.((F . n) - r).| < e / 2 by A84;

consider i being 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 being finite Subset of X such that

A89: not Y0 is empty and

A90: A . ii = Y0 and

A91: F . 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 :: thesis: for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e

hence
ex Y0 being finite Subset of X st |.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e

let Y1 be finite Subset of X; :: thesis: ( Y0 c= Y1 & Y1 c= Y implies |.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e )

assume that

A93: Y0 c= Y1 and

A94: Y1 c= Y ; :: thesis: |.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e

end;assume that

A93: Y0 c= Y1 and

A94: Y1 c= Y ; :: thesis: |.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e

now :: thesis: ( ( Y0 = Y1 & |.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) or ( Y0 <> Y1 & |.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )end;

hence
|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e
; :: thesis: verumper cases
( Y0 = Y1 or Y0 <> Y1 )
;

end;

case
Y0 = Y1
; :: thesis: |.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e

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 ; :: thesis: verum

end;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 ; :: thesis: verum

case A95:
Y0 <> Y1
; :: thesis: |.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e

ex Y2 being finite Subset of X st

( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 )

A97: ( not Y2 is 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; :: thesis: verum

end;( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 )

proof

then consider Y2 being finite Subset of X such that
take Y2 = Y1 \ Y0; :: thesis: ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 )

A96: Y1 \ Y0 c= Y1 by XBOOLE_1:36;

Y0 \/ Y2 = Y0 \/ Y1 by XBOOLE_1:39

.= Y1 by A93, XBOOLE_1:12 ;

hence ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 ) by A94, A95, A96, XBOOLE_1:79; :: thesis: verum

end;A96: Y1 \ Y0 c= Y1 by XBOOLE_1:36;

Y0 \/ Y2 = Y0 \/ Y1 by XBOOLE_1:39

.= Y1 by A93, XBOOLE_1:12 ;

hence ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 ) by A94, A95, A96, XBOOLE_1:79; :: thesis: verum

A97: ( not Y2 is 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; :: thesis: verum

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) by A89, A90; :: thesis: verum

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) ; :: thesis: verum