theorem Th28: :: CALCUL_1:28

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