deffunc H₁( Element of Funcs A,B) -> Element of bool [:A,B:] = (Q * $1) * (P " );
A1: for f being Element of Funcs A,B holds H₁(f) in Funcs A,B by FUNCT_2:11;
consider F being Function of (Funcs A,B),(Funcs A,B) such that
A2: for f being Element of Funcs A,B holds F . f = H₁(f) from FUNCT_2:sch 8(A1);
take F ; :: thesis: for f being Function of A,B holds F . f = (Q * f) * (P " )
let f be Function of A,B; :: thesis: F . f = (Q * f) * (P " )
f in Funcs A,B by FUNCT_2:11;
hence F . f = (Q * f) * (P " ) by A2; :: thesis: verum