:: deftheorem Def22 defines Segre_Blocks PENCIL_1:def 22 :
for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I
for b₃ being Subset-Family of (product (Carrier A)) holds
( b₃ = Segre_Blocks A iff for x being set holds
( x in b₃ iff ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) );