:: deftheorem defines NEx_Val SUBLEMMA:def 8 :
for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al
for x being bound_QC-variable of Al
for xSQ being second_Q_comp of [S,x]
for A being non empty set
for v being Element of Valuations_in (Al,A) holds NEx_Val (v,S,x,xSQ) = (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) * v;