set Al3 = Al1 \/ Al2;

( Al1 = [:NAT,(QC-symbols Al1):] & Al2 = [:NAT,(QC-symbols Al2):] ) by QC_LANG1:5;

then A1: Al1 \/ Al2 = [:NAT,((QC-symbols Al1) \/ (QC-symbols Al2)):] by ZFMISC_1:97;

NAT c= (QC-symbols Al1) \/ (QC-symbols Al2) by XBOOLE_1:10, QC_LANG1:3;

then reconsider Al3 = Al1 \/ Al2 as QC-alphabet by A1, QC_LANG1:def 1;

take Al3 ; :: thesis: ( Al3 is countable & Al3 is Al1 -expanding & Al3 is Al2 -expanding )

thus ( Al3 is countable & Al3 is Al1 -expanding & Al3 is Al2 -expanding ) by CARD_2:85, XBOOLE_1:7; :: thesis: verum

( Al1 = [:NAT,(QC-symbols Al1):] & Al2 = [:NAT,(QC-symbols Al2):] ) by QC_LANG1:5;

then A1: Al1 \/ Al2 = [:NAT,((QC-symbols Al1) \/ (QC-symbols Al2)):] by ZFMISC_1:97;

NAT c= (QC-symbols Al1) \/ (QC-symbols Al2) by XBOOLE_1:10, QC_LANG1:3;

then reconsider Al3 = Al1 \/ Al2 as QC-alphabet by A1, QC_LANG1:def 1;

take Al3 ; :: thesis: ( Al3 is countable & Al3 is Al1 -expanding & Al3 is Al2 -expanding )

thus ( Al3 is countable & Al3 is Al1 -expanding & Al3 is Al2 -expanding ) by CARD_2:85, XBOOLE_1:7; :: thesis: verum