let A be QC-alphabet ; 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; verum