theorem Th29: :: YELLOW16:30

for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I
for f being Element of (product J)
for X being Subset of (product J) holds
( f is_<=_than X iff for i being Element of I holds f . i is_<=_than pi (X,i) )