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:8;
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:8;
hence F . f = (Q * f) * (P ") by A2; :: thesis: verum