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 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 ) )
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 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
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;
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 ) ) 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 Y) - (setsum Y1)).|| < e ) ) ; :: thesis: verum
end;
hence Y is summable_set ; :: thesis: verum