:: deftheorem defines CQC_Subst SUBSTUT1:def 5 :
for A being QC-alphabet
for l being FinSequence of bound_QC-variables A
for Sub being CQC_Substitution of A holds CQC_Subst (l,Sub) = CQC_Subst ((@ l),Sub);