theorem Th24: :: PENCIL_1:24

for I being non empty set
for A being PLS-yielding ManySortedSet of I
for x being set holds
( x is Block of (Segre_Product A) iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) )