let X1, Y1, X2, Y2 be set ; :: thesis: for f1 being Function of X1,Y1
for f2 being Function of X2,Y2 st ( Y1 = {} implies X1 = {} ) & ( Y2 = {} implies X2 = {} ) holds
[:f1,f2:] = <:(f1 * (pr1 X1,X2)),(f2 * (pr2 X1,X2)):>
let f1 be Function of X1,Y1; :: thesis: for f2 being Function of X2,Y2 st ( Y1 = {} implies X1 = {} ) & ( Y2 = {} implies X2 = {} ) holds
[:f1,f2:] = <:(f1 * (pr1 X1,X2)),(f2 * (pr2 X1,X2)):>
let f2 be Function of X2,Y2; :: thesis: ( ( Y1 = {} implies X1 = {} ) & ( Y2 = {} implies X2 = {} ) implies [:f1,f2:] = <:(f1 * (pr1 X1,X2)),(f2 * (pr2 X1,X2)):> )
assume ( ( Y1 = {} implies X1 = {} ) & ( Y2 = {} implies X2 = {} ) ) ; :: thesis: [:f1,f2:] = <:(f1 * (pr1 X1,X2)),(f2 * (pr2 X1,X2)):>
then ( dom f1 = X1 & dom f2 = X2 ) by FUNCT_2:def 1;
hence [:f1,f2:] = <:(f1 * (pr1 X1,X2)),(f2 * (pr2 X1,X2)):> by Th87; :: thesis: verum