deffunc H₁( set ) -> set = (f1 . $1) * ((f2 . $1) " );
ex f being Function st
( dom f = (dom f1) /\ ((dom f2) \ (f2 " {0 })) & ( for x being set st x in (dom f1) /\ ((dom f2) \ (f2 " {0 })) holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
hence ex b₁ being Function st
( dom b₁ = (dom f1) /\ ((dom f2) \ (f2 " {0 })) & ( for c being set st c in dom b₁ holds
b₁ . c = (f1 . c) * ((f2 . c) " ) ) ) ; :: thesis: verum