theorem Th63: :: CALCUL_1:64

for Al being QC-alphabet holds
( card (bound_QC-variables Al) = card (QC-symbols Al) & not bound_QC-variables Al is finite )