deffunc H_{4}( Element of [:(bool D1),(bool D2):]) -> Element of bool D = f .: [:($1 `1),($1 `2):];

ex f being Function of [:(bool D1),(bool D2):],(bool D) st

for x being Element of [:(bool D1),(bool D2):] holds f . x = H_{4}(x)
from FUNCT_2:sch 4();

hence ex b_{1} being Function of [:(bool D1),(bool D2):],(bool D) st

for x being Element of [:(bool D1),(bool D2):] holds b_{1} . x = f .: [:(x `1),(x `2):]
; :: thesis: verum

ex f being Function of [:(bool D1),(bool D2):],(bool D) st

for x being Element of [:(bool D1),(bool D2):] holds f . x = H

hence ex b

for x being Element of [:(bool D1),(bool D2):] holds b