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

for L being linear-Functional of X st L is Lipschitzian holds

Y is_summable_set_by L )

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

for L being linear-Functional of X st L is Lipschitzian holds

Y is_summable_set_by L

let Y be Subset of X; :: thesis: ( Y is weakly_summable_set implies for L being linear-Functional of X st L is Lipschitzian holds

Y is_summable_set_by L )

assume Y is weakly_summable_set ; :: thesis: for L being linear-Functional of X st L is Lipschitzian holds

Y is_summable_set_by L

then consider x being Point of X such that

A2: for L being linear-Functional of X st L is Lipschitzian 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

|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) by A1, Th6;

let L be linear-Functional of X; :: thesis: ( L is Lipschitzian implies Y is_summable_set_by L )

assume L is Lipschitzian ; :: thesis: Y is_summable_set_by L

then 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

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

hence Y is_summable_set_by L ; :: thesis: verum

for L being linear-Functional of X st L is Lipschitzian holds

Y is_summable_set_by L )

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

for L being linear-Functional of X st L is Lipschitzian holds

Y is_summable_set_by L

let Y be Subset of X; :: thesis: ( Y is weakly_summable_set implies for L being linear-Functional of X st L is Lipschitzian holds

Y is_summable_set_by L )

assume Y is weakly_summable_set ; :: thesis: for L being linear-Functional of X st L is Lipschitzian holds

Y is_summable_set_by L

then consider x being Point of X such that

A2: for L being linear-Functional of X st L is Lipschitzian 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

|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) by A1, Th6;

let L be linear-Functional of X; :: thesis: ( L is Lipschitzian implies Y is_summable_set_by L )

assume L is Lipschitzian ; :: thesis: Y is_summable_set_by L

then 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

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

hence Y is_summable_set_by L ; :: thesis: verum