let X be RealLinearSpace; :: thesis: for A being finite Subset of X holds RAT_Sums A is countable
let A be finite Subset of X; :: thesis: RAT_Sums A is countable
set D = RAT_Sums A;
defpred S₁[ Nat] means for B being finite Subset of X st card B <= $1 holds
RAT_Sums B is countable ;

A2: now :: thesis: for B being finite Subset of X
for E being set st card B <= 0 holds
RAT_Sums B is countable

let B be finite Subset of X; :: thesis: for E being set st card B <= 0 holds
RAT_Sums B is countable
let E be set ; :: thesis: ( card B <= 0 implies RAT_Sums B is countable )
assume card B <= 0 ; :: thesis: RAT_Sums B is countable
then B = {} X ;
hence RAT_Sums B is countable by Lm13; :: thesis: verum

end;

then A4: S₁[ 0 ] ;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]

hereby :: thesis: verum

let B be finite Subset of X; :: thesis: ( card B <= k + 1 implies RAT_Sums b₁ is countable )
assume A7: card B <= k + 1 ; :: thesis: RAT_Sums b₁ is countable
set E = RAT_Sums B;

per cases ( card B = 0 or card B <> 0 ) ;

suppose card B = 0 ; :: thesis: RAT_Sums b₁ is countable

hence RAT_Sums B is countable by A2; :: thesis: verum

end;

suppose card B <> 0 ; :: thesis: RAT_Sums b₁ is countable

then B <> {} ;
then consider v being object such that
A8: v in B by XBOOLE_0:def 1;
reconsider v = v as Element of X by A8;
A9: (B \ {v}) \/ {v} = B by A8, XBOOLE_1:45, ZFMISC_1:31;
v in {v} by TARSKI:def 1;
then not v in B \ {v} by XBOOLE_0:def 5;
then A10: card ((B \ {v}) \/ {v}) = (card (B \ {v})) + 1 by CARD_2:41;
set D1 = RAT_Sums (B \ {v});
set D2 = RAT_Sums {v};
A11: RAT_Sums B = (RAT_Sums (B \ {v})) + (RAT_Sums {v}) by A9, Th12, XBOOLE_1:79;
( RAT_Sums (B \ {v}) is countable & RAT_Sums {v} is countable ) by A6, A7, A9, A10, Lm6, XREAL_1:6;
hence RAT_Sums B is countable by A11, Th5; :: thesis: verum

end;

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A5);
then S₁[ card A] ;
hence RAT_Sums A is countable ; :: thesis: verum