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

now :: thesis: for x being object holds
( ( x in RAT_Sums ({} X) implies x = 0. X ) & ( x = 0. X implies x in RAT_Sums ({} X) ) )

let x be object ; :: thesis: ( ( x in RAT_Sums ({} X) implies x = 0. X ) & ( x = 0. X implies x in RAT_Sums ({} X) ) )

hereby :: thesis: ( x = 0. X implies x in RAT_Sums ({} X) )

assume x in RAT_Sums ({} X) ; :: thesis: x = 0. X
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: verum

end;

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

now :: thesis: for a being object st a in rng (ZeroLC X) holds
a in RAT

let a be object ; :: thesis: ( a in rng (ZeroLC X) implies a in RAT )
assume a in rng (ZeroLC X) ; :: thesis: a in RAT
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: verum

end;

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

end;

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