deffunc H₁( Function) -> Element of BOOLEAN = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = $1 . y } ;
consider f being Function of (Valuations_in (Al,A)),BOOLEAN such that
A1: for v being Element of Valuations_in (Al,A) holds f . v = H₁(v) from FUNCT_2:sch 4();
( dom f = Valuations_in (Al,A) & rng f c= BOOLEAN ) by FUNCT_2:def 1, RELAT_1:def 19;
then reconsider f = f as Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:def 2;
take f ; :: thesis: for v being Element of Valuations_in (Al,A) holds f . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y }
thus for v being Element of Valuations_in (Al,A) holds f . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y } by A1; :: thesis: verum