theorem Th2: :: CQC_LANG:2

for A being QC-alphabet
for x being bound_QC-variable of A
for a being free_QC-variable of A holds a .--> x is Substitution of A