let I be non empty set ; :: thesis:
let A be PLS-yielding ManySortedSet of I; :: thesis:
assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis:
let B be set ; :: thesis:
thus ( B is Segre-Coset of A implies ex W being Subset of (Segre_Product A) st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) ) :: thesis:

assume B is Segre-Coset of A ; :: thesis:
then reconsider BB = B as Segre-Coset of A ;
consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A2: BB = product L and
A3: L . (indx L) = [#] (A . (indx L)) by Def2;
set K1 = the Block of (A . (indx L));
consider V being object such that
A4: V in product L by XBOOLE_0:def 1;
the Block of (A . (indx L)) in the topology of (A . (indx L)) ;
then reconsider K = the Block of (A . (indx L)) as Subset of (A . (indx L)) ;
A5: ex g being Function st
( g = V & dom g = dom L & ( for i being object st i in dom L holds
g . i in L . i ) ) by A4, CARD_3:def 5;
A6: dom L = I by PARTFUN1:def 2;
then reconsider V = V as ManySortedSet of I by A5, PARTFUN1:def 2, RELAT_1:def 18;
for i being object st i in I holds
V . i is Element of (Carrier A) . i

let i be object ; :: thesis:
assume A7: i in I ; :: thesis:
L c= Carrier A by PBOOLE:def 18;
then A8: L . i c= (Carrier A) . i by A7;
V . i in L . i by A6, A5, A7;
hence V . i is Element of (Carrier A) . i by A8; :: thesis:

end;

then reconsider V = V as Element of Carrier A by PBOOLE:def 14;
reconsider VV = {V} as ManySortedSubset of Carrier A by PENCIL_1:11;
reconsider X = VV +* ((indx L),K) as ManySortedSubset of Carrier A by Th7;
2 c= card K by PENCIL_1:def 6;
then A9: not K is trivial by PENCIL_1:4;
then reconsider X = X as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10;
dom VV = I by PARTFUN1:def 2;
then A10: X . (indx L) = K by FUNCT_7:31;
then indx X = indx L by A9, PENCIL_1:def 21;
then reconsider pX = product X as Block of (Segre_Product A) by A10, PENCIL_1:24;
A11: for i being object st i in I holds
X . i c= L . i

let i be object ; :: thesis:
assume A12: i in I ; :: thesis:

suppose i <> indx L ; :: thesis:

then X . i = VV . i by FUNCT_7:32;
then A13: X . i = {(V . i)} by A12, PZFMISC1:def 1;
V . i in L . i by A6, A5, A12;
hence X . i c= L . i by A13, ZFMISC_1:31; :: thesis:

end;

suppose i = indx L ; :: thesis:

hence X . i c= L . i by A3, A10; :: thesis:

end;

end;

end;

pX in the topology of (Segre_Product A) ;
then reconsider psX = pX as Subset of (Segre_Product A) ;
take psX ; :: thesis:
thus A14: ( not psX is trivial & psX is strong & psX is closed_under_lines ) by PENCIL_1:20, PENCIL_1:21; :: thesis:
then reconsider Z = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } as Segre-Coset of A by A1, Th22;
psX,psX are_joinable by A14, Th10;
then A15: psX in { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } by A14;
A16: psX c= Z by A15, TARSKI:def 4;
dom X = I by PARTFUN1:def 2;
then psX c= B by A2, A6, A11, CARD_3:27;
then psX c= B /\ Z by A16, XBOOLE_1:19;
then A17: card psX c= card (B /\ Z) by CARD_1:11;
2 c= card pX by PENCIL_1:def 6;
then BB = Z by A17, Th8, XBOOLE_1:1;
hence B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } ; :: thesis:

end;

given W being Subset of (Segre_Product A) such that A18: ( not W is trivial & W is strong & W is closed_under_lines ) and
A19: B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ; :: thesis:
thus B is Segre-Coset of A by A1, A18, A19, Th22; :: thesis: