theorem :: SUBLEMMA:64

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for v, w being Element of Valuations_in (Al,A)
for a being Element of A st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
(v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p)