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 S1[ 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 S1[n,X1] ;
consider E being Function of NAT,(bool the carrier of X) such that
A3: for n being Element of NAT holds S1[n,E . n] from 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 ;
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 ;
then A7: z in E . nmax by A4, A6;
dom E = NAT by FUNCT_2:def 1;
hence z in Union E by ; :: 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