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:
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:
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:
set E = RAT_Sums B;
per cases ( card B = 0 or card B <> 0 ) ;
suppose card B <> 0 ; :: thesis:
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 ;
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})) + () by ;
( RAT_Sums (B \ {v}) is countable & RAT_Sums {v} is countable ) by ;
hence RAT_Sums B is countable by ; :: 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