theorem Th7: :: SUBSTUT2:7

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 st x in rng (RestrictSub (x,(All (x,p)),Sub)) holds
S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p))