for f being non-empty Function
for X, Y being non empty set
for i, j being object st i in dom f & j in dom f & ( not X c= f . i or not f . j c= Y ) & product (f +* (i,X)) c= product (f +* (j,Y)) holds
( i = j & X c= Y )