theorem :: SUBLEMMA:32

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al st x in dom (S `2) holds
v . ((@ (S `2)) . x) = (v . (Val_S (v,S))) . x