theorem Th22: :: PENCIL_3:22

for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is connected ) holds
for i being Element of I
for p being Point of (A . i)
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds
ex D being FinSequence of bool the carrier of (Segre_Product A) st
( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds
D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )