deffunc H_{1}( Element of Funcs (A,B)) -> Element of bool [:A,B:] = (Q * $1) * (P ");

A1: for f being Element of Funcs (A,B) holds H_{1}(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_{1}(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

A1: for f being Element of Funcs (A,B) holds H

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

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