set A = (dom f) /\ (dom g);
deffunc H₁( object ) -> set = (f . $1) . (g . $1);
consider h being Function such that
A1: ( 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();
take h ; :: thesis: ( dom h = (dom f) /\ (dom g) & ( for x being set st x in dom h holds
h . x = (f . x) . (g . x) ) )
thus ( dom h = (dom f) /\ (dom g) & ( for x being set st x in dom h holds
h . x = (f . x) . (g . x) ) ) by A1; :: thesis: verum