theorem Th83: :: SUBLEMMA:83

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 @ (RestrictSub (x,(All (x,p)),Sub)) = (@ Sub) \ (((@ Sub) | (RSub1 (All (x,p)))) +* ((@ Sub) | (RSub2 ((All (x,p)),Sub))))