theorem Th9: :: SUBSTUT2:9

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for Sub being CQC_Substitution of Al holds ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub]))