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_{1}[ Nat] means for B being finite Subset of X st card B <= $1 holds

RAT_Sums B is countable ;

_{1}[ 0 ]
;

A5: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A4, A5);

then S_{1}[ card A]
;

hence RAT_Sums A is countable ; :: thesis: verum

let A be finite Subset of X; :: thesis: RAT_Sums A is countable

set D = RAT_Sums A;

defpred S

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

then A4:
Sfor 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;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

A5: for k being Nat st S

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A6: S_{1}[k]
; :: thesis: S_{1}[k + 1]

end;assume A6: S

hereby :: thesis: verum

let B be finite Subset of X; :: thesis: ( card B <= k + 1 implies RAT_Sums b_{1} is countable )

assume A7: card B <= k + 1 ; :: thesis: RAT_Sums b_{1} is countable

set E = RAT_Sums B;

end;assume A7: card B <= k + 1 ; :: thesis: RAT_Sums b

set E = RAT_Sums B;

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

end;

suppose
card B <> 0
; :: thesis: RAT_Sums b_{1} 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;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

then S

hence RAT_Sums A is countable ; :: thesis: verum