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;
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 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 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 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 Y1)).|| < e ) )
proof
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 Y1)).|| < e ) )

now :: thesis: for Y1 being finite Subset of X st Y c= Y1 & Y1 c= Y holds
||.(() - (setsum Y1)).|| < e
let Y1 be finite Subset of X; :: thesis: ( Y c= Y1 & Y1 c= Y implies ||.(() - (setsum Y1)).|| < e )
assume ( Y c= Y1 & Y1 c= Y ) ; :: thesis: ||.(() - (setsum Y1)).|| < e
then Y1 = Y by XBOOLE_0:def 10;
then (setsum Y) - (setsum Y1) = 0. X by RLVECT_1:15;
hence ||.(() - (setsum Y1)).|| < e by ; :: thesis: verum
end;
hence ( not Y is empty & Y c= Y & ( for Y1 being finite Subset of X st Y c= Y1 & Y1 c= Y holds
||.(() - (setsum Y1)).|| < e ) ) by A1; :: thesis: verum
end;
hence 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 Y1)).|| < e ) ) ; :: thesis: verum
end;
hence Y is summable_set ; :: thesis: verum