theorem Th5: :: CQC_LANG:5

for A being QC-alphabet
for k being Nat
for l being QC-variable_list of k,A holds
( l is CQC-variable_list of k,A iff ( { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) )