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