:: deftheorem defines variables_in QC_LANG3:def 1 :
for A being QC-alphabet
for l being FinSequence of QC-variables A
for V being non empty Subset of (QC-variables A) holds variables_in (l,V) = { (l . k) where k is Nat : ( 1 <= k & k <= len l & l . k in V ) } ;