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_{1}[ 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_{1}[n,X1]
;

consider E being Function of NAT,(bool the carrier of X) such that

A3: for n being Element of NAT holds S_{1}[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

for n being set st n in dom E holds

E . n is countable

hence RAT_Sums (rng x) is countable by A8; :: thesis: verum

let x be sequence of X; :: thesis: RAT_Sums (rng x) is countable

set D = RAT_Sums (rng x);

defpred S

A2: for n being Element of NAT ex X1 being Element of bool the carrier of X st S

consider E being Function of NAT,(bool the carrier of X) such that

A3: for n being Element of NAT holds S

for z being object st z in RAT_Sums (rng x) holds

z in Union E

proof

then A8:
RAT_Sums (rng x) c= Union E
;
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;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

for n being set st n in dom E holds

E . n is countable

proof

then
Union E is countable
by CARD_4:11;
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;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

hence RAT_Sums (rng x) is countable by A8; :: thesis: verum