:: deftheorem defines Sub_Var SUBSTUT1:def 10 :
for A being QC-alphabet
for finSub being finite CQC_Substitution of A holds Sub_Var finSub = { s where s is QC-symbol of A : x. s in rng finSub } ;