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 S1[ 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: S1[ 0 ] ;
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; :: thesis: S1[k + 1]
hereby :: thesis: verum
let B be finite Subset of X; :: thesis: ( card B <= k + 1 implies RAT_Sums b1 is countable )
assume A7: card B <= k + 1 ; :: thesis: RAT_Sums b1 is countable
set E = RAT_Sums B;
per cases ( card B = 0 or card B <> 0 ) ;
suppose card B <> 0 ; :: thesis: RAT_Sums b1 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 S1[k] from NAT_1:sch 2(A4, A5);
 then S1[ card A] ;
hence RAT_Sums A is countable ; :: thesis: verum