deffunc H₁( Element of bool the carrier of R) -> Element of bool the carrier of R = LAp $1;
ex f being Function of (bool the carrier of R),(bool the carrier of R) st
for X being Element of bool the carrier of R holds f . X = H₁(X) from FUNCT_2:sch 4();
then consider f being Function of (bool the carrier of R),(bool the carrier of R) such that
A1: for X being Subset of R holds f . X = H₁(X) ;
take f ; :: thesis: for X being Subset of R holds f . X = LAp X
let r be Subset of R; :: thesis: f . r = LAp r
thus f . r = LAp r by A1; :: thesis: verum