let X be RealUnitarySpace; :: thesis: for Y being finite Subset of X st not Y is empty holds

Y is summable_set

let Y be finite Subset of X; :: thesis: ( not Y is empty implies Y is summable_set )

assume A1: not Y is empty ; :: thesis: Y is summable_set

set x = setsum Y;

Y is summable_set

let Y be finite Subset of X; :: thesis: ( not Y is empty implies Y is summable_set )

assume A1: not Y is empty ; :: thesis: Y is summable_set

set x = setsum Y;

now :: 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

||.((setsum Y) - (setsum Y1)).|| < e ) )

hence
Y is summable_set
; :: thesis: verumex 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

||.((setsum Y) - (setsum Y1)).|| < e ) )

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

||.((setsum Y) - (setsum Y1)).|| < e ) ) )

assume A2: 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

||.((setsum Y) - (setsum Y1)).|| < 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

||.((setsum Y) - (setsum Y1)).|| < e ) )

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

||.((setsum Y) - (setsum Y1)).|| < e ) ) ; :: 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

||.((setsum Y) - (setsum Y1)).|| < e ) ) )

assume A2: 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

||.((setsum Y) - (setsum Y1)).|| < 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

||.((setsum Y) - (setsum Y1)).|| < e ) )

proof

hence
ex Y0 being finite Subset of X st
take
Y
; :: thesis: ( not Y is empty & Y c= Y & ( for Y1 being finite Subset of X st Y c= Y1 & Y1 c= Y holds

||.((setsum Y) - (setsum Y1)).|| < e ) )

||.((setsum Y) - (setsum Y1)).|| < e ) ) by A1; :: thesis: verum

end;||.((setsum Y) - (setsum Y1)).|| < e ) )

now :: thesis: for Y1 being finite Subset of X st Y c= Y1 & Y1 c= Y holds

||.((setsum Y) - (setsum Y1)).|| < e

hence
( not Y is empty & Y c= Y & ( for Y1 being finite Subset of X st Y c= Y1 & Y1 c= Y holds ||.((setsum Y) - (setsum Y1)).|| < e

let Y1 be finite Subset of X; :: thesis: ( Y c= Y1 & Y1 c= Y implies ||.((setsum Y) - (setsum Y1)).|| < e )

assume ( Y c= Y1 & Y1 c= Y ) ; :: thesis: ||.((setsum Y) - (setsum Y1)).|| < e

then Y1 = Y by XBOOLE_0:def 10;

then (setsum Y) - (setsum Y1) = 0. X by RLVECT_1:15;

hence ||.((setsum Y) - (setsum Y1)).|| < e by A2, BHSP_1:26; :: thesis: verum

end;assume ( Y c= Y1 & Y1 c= Y ) ; :: thesis: ||.((setsum Y) - (setsum Y1)).|| < e

then Y1 = Y by XBOOLE_0:def 10;

then (setsum Y) - (setsum Y1) = 0. X by RLVECT_1:15;

hence ||.((setsum Y) - (setsum Y1)).|| < e by A2, BHSP_1:26; :: thesis: verum

||.((setsum Y) - (setsum Y1)).|| < e ) ) by A1; :: thesis: verum

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

||.((setsum Y) - (setsum Y1)).|| < e ) ) ; :: thesis: verum