:: deftheorem defines Segre_Product PENCIL_1:def 23 :
for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I holds Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #);