deffunc H₁( Element of NAT ) -> Element of bool Omega = X /\ (f . $1);
consider g being sequence of (bool Omega) such that
A1: for x being Element of NAT holds g . x = H₁(x) from FUNCT_2:sch 4();
take g ; :: thesis: for n being Element of NAT holds g . n = X /\ (f . n)
let n be Element of NAT ; :: thesis: g . n = X /\ (f . n)
thus g . n = X /\ (f . n) by A1; :: thesis: verum