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