let X be addLoopStr ; :: thesis: for A, B being Subset of X st A is countable & B is countable holds

A + B is countable

let A, B be Subset of X; :: thesis: ( A is countable & B is countable implies A + B is countable )

assume A1: ( A is countable & B is countable ) ; :: thesis: A + B is countable

set D = A + B;

A + B is countable

let A, B be Subset of X; :: thesis: ( A is countable & B is countable implies A + B is countable )

assume A1: ( A is countable & B is countable ) ; :: thesis: A + B is countable

set D = A + B;

per cases
( A is empty or B is empty or ( not A is empty & not B is empty ) )
;

end;

suppose A2:
( A is empty or B is empty )
; :: thesis: A + B is countable

end;

now :: thesis: not A + B <> {}

hence
A + B is countable
; :: thesis: verumassume
A + B <> {}
; :: thesis: contradiction

then consider x being object such that

A3: x in A + B by XBOOLE_0:def 1;

A + B = { (a + b) where a, b is Point of X : ( a in A & b in B ) } by IDEAL_1:def 19;

then ex a, b being Point of X st

( x = a + b & a in A & b in B ) by A3;

hence contradiction by A2; :: thesis: verum

end;then consider x being object such that

A3: x in A + B by XBOOLE_0:def 1;

A + B = { (a + b) where a, b is Point of X : ( a in A & b in B ) } by IDEAL_1:def 19;

then ex a, b being Point of X st

( x = a + b & a in A & b in B ) by A3;

hence contradiction by A2; :: thesis: verum

suppose A4:
( not A is empty & not B is empty )
; :: thesis: A + B is countable

consider F being Function of (A + B),[:A,B:] such that

A5: F is one-to-one by Th4;

( dom F = A + B & rng F c= [:A,B:] ) by A4, FUNCT_2:def 1;

then A6: card (A + B) c= card [:A,B:] by A5, CARD_1:10;

[:A,B:] is countable by A1, CARD_4:7;

then card [:A,B:] c= omega ;

then card (A + B) c= omega by A6;

hence A + B is countable ; :: thesis: verum

end;A5: F is one-to-one by Th4;

( dom F = A + B & rng F c= [:A,B:] ) by A4, FUNCT_2:def 1;

then A6: card (A + B) c= card [:A,B:] by A5, CARD_1:10;

[:A,B:] is countable by A1, CARD_4:7;

then card [:A,B:] c= omega ;

then card (A + B) c= omega by A6;

hence A + B is countable ; :: thesis: verum