for Y, Z being set
for f, g being Function st dom f = dom g & rng f c= Y & rng g c= Z holds
( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g )