let X be RealLinearSpace; :: thesis: for x being sequence of X holds RAT_Sums (rng x) is countable
let x be sequence of X; :: thesis: RAT_Sums (rng x) is countable
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

proof

let z be object ; :: thesis: ( z in RAT_Sums (rng x) implies z in Union E )
assume z in RAT_Sums (rng x) ; :: thesis: z in Union E
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: verum

end;

then A8: RAT_Sums (rng x) c= Union E ;
for n being set st n in dom E holds
E . n is countable

proof

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

end;

then Union E is countable by CARD_4:11;
hence RAT_Sums (rng x) is countable by A8; :: thesis: verum