theorem :: SUBSTUT1:39

for A being QC-alphabet
for Sub being CQC_Substitution of A holds rng (@ Sub) c= bound_QC-variables A ;