deffunc H_{1}( 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_{1}(x)
from FUNCT_2:sch 4();

thus ex b_{1} 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_{1} . x = <.(U_FMT x).]
by A1; :: thesis: verum

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

thus ex b

for x being Element of the carrier of ET holds b