for f, g being Function holds [:f,g:] = <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):>