theorem :: FUNCT_3:77

for X1, X2 being set
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))):>