for x being Element of Valuations_in A holds x is Function of bound_QC-variables,A by Th2;
hence Valuations_in A is FUNCTION_DOMAIN of bound_QC-variables ,A by FUNCT_2:def 13; :: thesis: verum