theorem Th16: :: PENCIL_3:16

for I being non empty set
for i being Element of I
for A being PLS-yielding ManySortedSet of I
for B being Block of (A . i)
for P being Element of Carrier A holds product ({P} +* (i,B)) is Block of (Segre_Product A)