deffunc H₁( Element of the carrier of ET) -> Element of K24(K24( the carrier of ET)) = <.(U_FMT $1).];
consider f being Function of the carrier of ET,(bool (bool the carrier of ET)) such that
A1: for x being Element of the carrier of ET holds f . x = H₁(x) from FUNCT_2:sch 4();
thus ex b₁ being Function of the carrier of ET,(bool (bool the carrier of ET)) st
for x being Element of the carrier of ET holds b₁ . x = <.(U_FMT x).] by A1; :: thesis: verum