theorem Th25: :: PENCIL_1:25

for I being non empty set
for A being PLS-yielding ManySortedSet of I
for P being ManySortedSet of I st P is Point of (Segre_Product A) holds
for i being Element of I
for p being Point of (A . i) holds P +* (i,p) is Point of (Segre_Product A)