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_{1}[ 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_{1}[x,y] )

A4: for x being object st x in RAT_Sums {v} holds

S_{1}[x,F . x]
from FUNCT_2:sch 1(A2);

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

let v be Element of the carrier of X; :: thesis: RAT_Sums {v} is countable

set D = RAT_Sums {v};

defpred S

( $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

proof

consider F being Function of (RAT_Sums {v}),RAT such that
let x be object ; :: thesis: ( x in RAT_Sums {v} implies ex y being object st

( y in RAT & S_{1}[x,y] ) )

assume x in RAT_Sums {v} ; :: thesis: ex y being object st

( y in RAT & S_{1}[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_{1}[x,y] )

dom l = the carrier of X by FUNCT_2:def 1;

hence y in RAT by A3, FUNCT_1:3; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A3; :: thesis: verum

end;( y in RAT & S

assume x in RAT_Sums {v} ; :: thesis: ex y being object st

( y in RAT & S

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

dom l = the carrier of X by FUNCT_2:def 1;

hence y in RAT by A3, FUNCT_1:3; :: thesis: S

thus S

A4: for x being object st x in RAT_Sums {v} holds

S

now :: thesis: for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds

x1 = x2

then A8:
F is one-to-one
;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;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

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