for Al being QC-alphabet
for p being Element of CQC-WFF Al
for Sub being CQC_Substitution of Al holds dom ((@ Sub) | (RSub1 p)) misses dom ((@ Sub) | (RSub2 (p,Sub)))