:: deftheorem defines Valuations_in VALUAT_1:def 1 :
for Al being QC-alphabet
for A being set holds Valuations_in (Al,A) = Funcs ((bound_QC-variables Al),A);