deffunc H₄( 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₄(x) from FUNCT_2:sch 4();
hence ex b₁ being Function of [:(bool D1),(bool D2):],(bool D) st
for x being Element of [:(bool D1),(bool D2):] holds b₁ . x = f .: [:(x `1),(x `2):] ; :: thesis: verum