:: deftheorem defines Bound_Vars SUBSTUT1:def 7 :
for A being QC-alphabet
for l1 being FinSequence of QC-variables A holds Bound_Vars l1 = { (l1 . k) where k is Nat : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) } ;