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