let X be RealUnitarySpace; :: thesis: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity implies for Y being Subset of X st Y is weakly_summable_set holds
ex x being Point of X st
for L being linear-Functional of X st L is Bounded holds
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
abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) ) )
assume A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity ) ; :: thesis: for Y being Subset of X st Y is weakly_summable_set holds
ex x being Point of X st
for L being linear-Functional of X st L is Bounded holds
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
abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) )
let Y be Subset of X; :: thesis: ( Y is weakly_summable_set implies ex x being Point of X st
for L being linear-Functional of X st L is Bounded holds
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
abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) ) )
assume Y is weakly_summable_set ; :: thesis: ex x being Point of X st
for L being linear-Functional of X st L is Bounded holds
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
abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) )
then consider x being Point of X such that
A2: for L being linear-Functional of X st L is Bounded holds
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
abs (L . (x - (setsum Y1))) < e ) ) by Def5;
take x ; :: thesis: for L being linear-Functional of X st L is Bounded holds
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
abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) )

now

let L be linear-Functional of X; :: thesis: ( L is Bounded implies 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
abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) ) )
assume A3: L is Bounded ; :: thesis: 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
abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) )

now

let e be Real; :: thesis: ( e > 0 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
abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) ) )
assume A4: 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
abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) )
consider Y0 being finite Subset of X such that
A5: ( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (L . (x - (setsum Y1))) < e ) ) by A2, A3, A4;
take Y0 = Y0; :: thesis: ( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) )

now

let Y1 be finite Subset of X; :: thesis: ( Y0 c= Y1 & Y1 c= Y implies abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e )
assume A6: ( Y0 c= Y1 & Y1 c= Y ) ; :: thesis: abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e
set r = L . (x - (setsum Y1));
set x1 = x;
set y1 = setsum Y1;
A7: L . (x - (setsum Y1)) = (L . x) - (L . (setsum Y1)) by HAHNBAN:32;
Y1 <> {} by A5, A6;
then L . (setsum Y1) = setopfunc Y1,the carrier of X,REAL ,L,addreal by A1, Th5;
hence abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e by A5, A6, A7; :: thesis: verum

end;

hence ( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) ) by A5; :: thesis: verum

end;

hence 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
abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) ) ; :: thesis: verum

end;

hence for L being linear-Functional of X st L is Bounded holds
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
abs ((L . x) - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) ) ; :: thesis: verum