let X be RealLinearSpace; :: thesis: RAT_Sums ({} X) is countable

set A = {} X;

set D = RAT_Sums ({} X);

hence RAT_Sums ({} X) is countable ; :: thesis: verum

set A = {} X;

set D = RAT_Sums ({} X);

now :: thesis: for x being object holds

( ( x in RAT_Sums ({} X) implies x = 0. X ) & ( x = 0. X implies x in RAT_Sums ({} X) ) )

then
RAT_Sums ({} X) = {(0. X)}
by TARSKI:def 1;( ( x in RAT_Sums ({} X) implies x = 0. X ) & ( x = 0. X implies x in RAT_Sums ({} X) ) )

let x be object ; :: thesis: ( ( x in RAT_Sums ({} X) implies x = 0. X ) & ( x = 0. X implies x in RAT_Sums ({} X) ) )

A5: ZeroLC X is Linear_Combination of {} X by RLVECT_2:22;

A6: Sum (ZeroLC X) = 0. X by RLVECT_2:30;

thus x in RAT_Sums ({} X) by A4, A5, A6, A7; :: thesis: verum

end;hereby :: thesis: ( x = 0. X implies x in RAT_Sums ({} X) )

assume A4:
x = 0. X
; :: thesis: x in RAT_Sums ({} X)assume
x in RAT_Sums ({} X)
; :: thesis: x = 0. X

then consider l being Linear_Combination of {} X such that

A3: ( x = Sum l & rng l c= RAT ) ;

Carrier l c= {} X by RLVECT_2:def 6;

then Carrier l = {} ;

hence x = 0. X by A3, RLVECT_2:34; :: thesis: verum

end;then consider l being Linear_Combination of {} X such that

A3: ( x = Sum l & rng l c= RAT ) ;

Carrier l c= {} X by RLVECT_2:def 6;

then Carrier l = {} ;

hence x = 0. X by A3, RLVECT_2:34; :: thesis: verum

A5: ZeroLC X is Linear_Combination of {} X by RLVECT_2:22;

A6: Sum (ZeroLC X) = 0. X by RLVECT_2:30;

now :: thesis: for a being object st a in rng (ZeroLC X) holds

a in RAT

then A7:
rng (ZeroLC X) c= RAT
;a in RAT

let a be object ; :: thesis: ( a in rng (ZeroLC X) implies a in RAT )

assume a in rng (ZeroLC X) ; :: thesis: a in RAT

then ex x being Element of X st a = (ZeroLC X) . x by FUNCT_2:113;

then a = 0 by RLVECT_2:20;

hence a in RAT by RAT_1:def 2; :: thesis: verum

end;assume a in rng (ZeroLC X) ; :: thesis: a in RAT

then ex x being Element of X st a = (ZeroLC X) . x by FUNCT_2:113;

then a = 0 by RLVECT_2:20;

hence a in RAT by RAT_1:def 2; :: thesis: verum

thus x in RAT_Sums ({} X) by A4, A5, A6, A7; :: thesis: verum

hence RAT_Sums ({} X) is countable ; :: thesis: verum