let X be RealLinearSpace; :: thesis:
let x be sequence of X; :: thesis:
set D = RAT_Sums (rng x);
defpred S₁[ Nat, object ] means $2 = RAT_Sums (rng (x | (Segm $1)));
A2: for n being Element of NAT ex X1 being Element of bool the carrier of X st S₁[n,X1] ;
consider E being Function of NAT,(bool the carrier of X) such that
A3: for n being Element of NAT holds S₁[n,E . n] from FUNCT_2:sch 3(A2);
for z being object st z in RAT_Sums (rng x) holds
z in Union E

let z be object ; :: thesis:
assume z in RAT_Sums (rng x) ; :: thesis:
then consider l being Linear_Combination of rng x such that
A4: ( z = Sum l & rng l c= RAT ) ;
consider nmax being Nat such that
A5: Carrier l c= rng (x | (Segm nmax)) by RLVECT_2:def 6, Th15;
reconsider nmax = nmax as Element of NAT by ORDINAL1:def 12;
A6: E . nmax = RAT_Sums (rng (x | (Segm nmax))) by A3;
l is Linear_Combination of rng (x | nmax) by A5, RLVECT_2:def 6;
then A7: z in E . nmax by A4, A6;
dom E = NAT by FUNCT_2:def 1;
hence z in Union E by A7, CARD_5:2; :: thesis:

end;

let n be set ; :: thesis:
assume n in dom E ; :: thesis:
then reconsider n1 = n as Element of NAT ;
E . n = RAT_Sums (rng (x | (Segm n1))) by A3;
hence E . n is countable ; :: thesis:

end;