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: RAT_Sums {v} is countable
set D = RAT_Sums {v};
defpred S₁[ 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 & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in RAT_Sums {v} implies ex y being object st
( y in RAT & S₁[x,y] ) )
assume x in RAT_Sums {v} ; :: thesis: ex y being object st
( y in RAT & S₁[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 & S₁[x,y] )
dom l = the carrier of X by FUNCT_2:def 1;
hence y in RAT by A3, FUNCT_1:3; :: thesis: S₁[x,y]
thus S₁[x,y] by A3; :: thesis: verum

end;

consider F being Function of (RAT_Sums {v}),RAT such that
A4: for x being object st x in RAT_Sums {v} holds
S₁[x,F . x] from FUNCT_2:sch 1(A2);

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 A6, A7, RLVECT_2:32;
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 (RAT_Sums {v}) c= card RAT by A8, A9, CARD_1:10;
card RAT c= omega by CARD_3:def 14;
then card (RAT_Sums {v}) c= omega by A10;
hence RAT_Sums {v} is countable ; :: thesis: verum