theorem Th84: :: SUBLEMMA:84

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 dom (@ (RestrictSub (x,p,Sub))) misses (dom ((@ Sub) | (RSub1 p))) \/ (dom ((@ Sub) | (RSub2 (p,Sub))))