let X be RealLinearSpace; :: thesis: for v being Element of the carrier of X holds RAT_Sums {v} is countable
let v be Element of the carrier of X; :: thesis:
set D = RAT_Sums {v};
defpred S1[ object , object ] means ex l being Linear_Combination of {v} st
( \$1 = Sum l & rng l c= RAT & \$2 = l . v );
A2: for x being object st x in RAT_Sums {v} holds
ex y being object st
( y in RAT & S1[x,y] )
proof
let x be object ; :: thesis: ( x in RAT_Sums {v} implies ex y being object st
( y in RAT & S1[x,y] ) )

assume x in RAT_Sums {v} ; :: thesis: ex y being object st
( y in RAT & S1[x,y] )

then consider l being Linear_Combination of {v} such that
A3: ( x = Sum l & rng l c= RAT ) ;
take y = l . v; :: thesis: ( y in RAT & S1[x,y] )
dom l = the carrier of X by FUNCT_2:def 1;
hence y in RAT by ; :: thesis: S1[x,y]
thus S1[x,y] by A3; :: thesis: verum
end;
consider F being Function of (),RAT such that
A4: for x being object st x in RAT_Sums {v} holds
S1[x,F . x] from
now :: thesis: for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume A5: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 ) ; :: thesis: x1 = x2
then consider l1 being Linear_Combination of {v} such that
A6: ( x1 = Sum l1 & rng l1 c= RAT & F . x1 = l1 . v ) by A4;
consider l2 being Linear_Combination of {v} such that
A7: ( x2 = Sum l2 & rng l2 c= RAT & F . x2 = l2 . v ) by A4, A5;
( x1 = (l1 . v) * v & x2 = (l2 . v) * v ) by ;
hence x1 = x2 by A5, A6, A7; :: thesis: verum
end;
then A8: F is one-to-one ;
A9: dom F = RAT_Sums {v} by FUNCT_2:def 1;
rng F is countable ;
then A10: card () c= card RAT by ;
card RAT c= omega by CARD_3:def 14;
then card () c= omega by A10;
hence RAT_Sums {v} is countable ; :: thesis: verum