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;
per cases ( A is empty or B is empty or ( not A is empty & not B is empty ) ) ;
suppose A2: ( A is empty or B is empty ) ; :: thesis: A + B is countable
now :: thesis: not A + B <> {}
assume 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;
hence A + B is countable ; :: thesis: verum
end;
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;
end;