theorem Th31: :: TOPS_5:31

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