:: deftheorem defines Val_S SUBLEMMA:def 1 :
for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al
for A being non empty set
for v being Element of Valuations_in (Al,A) holds Val_S (v,S) = (@ (S `2)) * v;