for Al being QC-alphabet
for Al2 being b₁ -expanding QC-alphabet
for p2 being Element of CQC-WFF Al2
for S being finite CQC_Substitution of Al
for S2 being finite CQC_Substitution of Al2
for p being Element of CQC-WFF Al st S = S2 & p = p2 holds
upVar (S,p) = upVar (S2,p2)