let X, Y be set ; :: thesis: ( X is countable & Y is countable implies [:X,Y:] is countable )

assume ( card X c= omega & card Y c= omega ) ; :: according to CARD_3:def 14 :: thesis: [:X,Y:] is countable

then [:(card X),(card Y):] c= [:omega,omega:] by ZFMISC_1:96;

then card [:(card X),(card Y):] c= card [:omega,omega:] by CARD_1:11;

then card [:(card X),(card Y):] c= omega *` omega by CARD_2:def 2;

hence card [:X,Y:] c= omega by Th6, CARD_2:7; :: according to CARD_3:def 14 :: thesis: verum

assume ( card X c= omega & card Y c= omega ) ; :: according to CARD_3:def 14 :: thesis: [:X,Y:] is countable

then [:(card X),(card Y):] c= [:omega,omega:] by ZFMISC_1:96;

then card [:(card X),(card Y):] c= card [:omega,omega:] by CARD_1:11;

then card [:(card X),(card Y):] c= omega *` omega by CARD_2:def 2;

hence card [:X,Y:] c= omega by Th6, CARD_2:7; :: according to CARD_3:def 14 :: thesis: verum