let A be non empty set ; :: thesis: for x being set st x is Element of Valuations_in A holds
x is Function of bound_QC-variables ,A
let x be set ; :: thesis: ( x is Element of Valuations_in A implies x is Function of bound_QC-variables ,A )
assume x is Element of Valuations_in A ; :: thesis: x is Function of bound_QC-variables ,A
then ex f being Function st
( x = f & dom f = bound_QC-variables & rng f c= A ) by FUNCT_2:def 2;
hence x is Function of bound_QC-variables ,A by FUNCT_2:def 1, RELSET_1:11; :: thesis: verum