let X1, X2 be set ; :: thesis: for D1, D2 being non empty set
for f1 being Function of X1,D1
for f2 being Function of X2,D2 holds [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):>
let D1, D2 be non empty set ; :: thesis: for f1 being Function of X1,D1
for f2 being Function of X2,D2 holds [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):>
let f1 be Function of X1,D1; :: thesis: for f2 being Function of X2,D2 holds [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):>
let f2 be Function of X2,D2; :: thesis: [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):>
( 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