for x being Element of Valuations_in (Al,A) holds x is Function of (bound_QC-variables Al),A by Th1;
hence Valuations_in (Al,A) is FUNCTION_DOMAIN of bound_QC-variables Al,A by FUNCT_2:def 12; :: thesis: verum