let X be RealLinearSpace; :: thesis:
set A = {} X;
set D = RAT_Sums ({} X);

let x be object ; :: thesis:

hereby :: thesis:

assume x in RAT_Sums ({} X) ; :: thesis:
then consider l being Linear_Combination of {} X such that
A3: ( x = Sum l & rng l c= RAT ) ;
Carrier l c= {} X by RLVECT_2:def 6;
then Carrier l = {} ;
hence x = 0. X by A3, RLVECT_2:34; :: thesis:

end;

assume A4: x = 0. X ; :: thesis:
A5: ZeroLC X is Linear_Combination of {} X by RLVECT_2:22;
A6: Sum (ZeroLC X) = 0. X by RLVECT_2:30;

let a be object ; :: thesis:
assume a in rng (ZeroLC X) ; :: thesis:
then ex x being Element of X st a = (ZeroLC X) . x by FUNCT_2:113;
then a = 0 by RLVECT_2:20;
hence a in RAT by RAT_1:def 2; :: thesis:

end;

then A7: rng (ZeroLC X) c= RAT ;
thus x in RAT_Sums ({} X) by A4, A5, A6, A7; :: thesis:

end;

then RAT_Sums ({} X) = {(0. X)} by TARSKI:def 1;
hence RAT_Sums ({} X) is countable ; :: thesis: