theorem Th1: :: SUBSTUT1:1

for A being QC-alphabet
for a being object
for Sub being CQC_Substitution of A st a in dom Sub holds
Sub . a in bound_QC-variables A