let X1, X2, Y1, 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 Th66; :: thesis: verum