let A be QC-alphabet ; :: thesis: QC-variables A c= [:NAT,(QC-symbols A):]
( {6} c= NAT & NAT c= QC-symbols A ) by Th3, ZFMISC_1:31;
then A1: [:{6},NAT:] c= [:NAT,(QC-symbols A):] by ZFMISC_1:96;
( {4,5} c= NAT & QC-symbols A c= QC-symbols A ) by ZFMISC_1:32;
then [:{4,5},(QC-symbols A):] c= [:NAT,(QC-symbols A):] by ZFMISC_1:96;
hence QC-variables A c= [:NAT,(QC-symbols A):] by A1, XBOOLE_1:8; :: thesis: verum