deffunc H₁( Element of bool the carrier of R) -> Element of bool the carrier of R = UAp $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
A4: for X being Subset of R holds f . X = H₁(X) ;
take f ; :: thesis: for X being Subset of R holds f . X = UAp X
let r be Subset of R; :: thesis: f . r = UAp r
thus f . r = UAp r by A4; :: thesis: verum