deffunc H₁( object ) -> object = [(f . $1),(g . $1)];
ex fg being Function st
( dom fg = (dom f) /\ (dom g) & ( for x being object st x in (dom f) /\ (dom g) holds
fg . x = H₁(x) ) ) from FUNCT_1:sch 3();
hence ex b₁ being Function st
( dom b₁ = (dom f) /\ (dom g) & ( for x being object st x in dom b₁ holds
b₁ . x = [(f . x),(g . x)] ) ) ; :: thesis: verum