for f being Function
for A, B being set
for i, j being object st i in dom f & j in dom f & A c= f . i & B c= f . j holds
product (f +* ((i,j) --> (A,B))) c= product f