let X, Y, Z be set ; :: thesis: for f being Function of X,Y
for g being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) holds
( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g )
let f be Function of X,Y; :: thesis: for g being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) holds
( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g )
let g be Function of X,Z; :: thesis: ( ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) implies ( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g ) )
assume ( ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) ) ; :: thesis: ( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g )
then A1: ( dom f = X & dom g = X ) by FUNCT_2:def 1;
( rng f c= Y & rng g c= Z ) by RELAT_1:def 19;
hence ( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g ) by A1, Th72; :: thesis: verum