deffunc H₁( object ) -> set = (f . $1) /\ (g . $1);
thus ex h being Function st
( dom h = (dom f) /\ (dom g) & ( for x being object st x in (dom f) /\ (dom g) holds
h . x = H₁(x) ) ) from FUNCT_1:sch 3(); :: thesis: verum