theorem Th18: :: PENCIL_3:18

for I being non empty set
for A being PLS-yielding ManySortedSet of I
for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A
for x being Point of (A . (indx b)) ex p being ManySortedSet of I st
( p in product b & {(p +* ((indx b),x))} = product (b +* ((indx b),{x})) )