for X being non empty set
for Y being Subset of X
for i being object holds (proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y