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

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

assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis: for B being set holds
( B is Segre-Coset of A iff ex W being Subset of () st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) )

let B be set ; :: thesis: ( B is Segre-Coset of A iff ex W being Subset of () st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) )

thus ( B is Segre-Coset of A implies ex W being Subset of () st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) ) :: thesis: ( ex W being Subset of () st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) implies B is Segre-Coset of A )
proof
assume B is Segre-Coset of A ; :: thesis: ex W being Subset of () st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } )

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 ;
A6: dom L = I by PARTFUN1:def 2;
then reconsider V = V as ManySortedSet of I by ;
for i being object st i in I holds
V . i is Element of () . i
proof
let i be object ; :: thesis: ( i in I implies V . i is Element of () . i )
assume A7: i in I ; :: thesis: V . i is Element of () . i
L c= Carrier A by PBOOLE:def 18;
then A8: L . i c= () . i by A7;
V . i in L . i by A6, A5, A7;
hence V . i is Element of () . i by A8; :: thesis: verum
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 ;
dom VV = I by PARTFUN1:def 2;
then A10: X . (indx L) = K by FUNCT_7:31;
then indx X = indx L by ;
then reconsider pX = product X as Block of () by ;
A11: for i being object st i in I holds
X . i c= L . i
proof
let i be object ; :: thesis: ( i in I implies X . i c= L . i )
assume A12: i in I ; :: thesis: X . i c= L . i
per cases ( i <> indx L or i = indx L ) ;
suppose i <> indx L ; :: thesis: X . i c= L . i
then X . i = VV . i by FUNCT_7:32;
then A13: X . i = {(V . i)} by ;
V . i in L . i by A6, A5, A12;
hence X . i c= L . i by ; :: thesis: verum
end;
suppose i = indx L ; :: thesis: X . i c= L . i
hence X . i c= L . i by ; :: thesis: verum
end;
end;
end;
pX in the topology of () ;
then reconsider psX = pX as Subset of () ;
take psX ; :: thesis: ( not psX is trivial & psX is strong & psX is closed_under_lines & B = union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } )
thus A14: ( not psX is trivial & psX is strong & psX is closed_under_lines ) by ; :: thesis: B = union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) }
then reconsider Z = union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } as Segre-Coset of A by ;
psX,psX are_joinable by ;
then A15: psX in { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } by A14;
A16: psX c= Z by ;
dom X = I by PARTFUN1:def 2;
then psX c= B by ;
then psX c= B /\ Z by ;
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 ;
hence B = union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & psX,Y are_joinable ) } ; :: thesis: verum
end;
given W being Subset of () 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 () : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ; :: thesis: B is Segre-Coset of A
thus B is Segre-Coset of A by A1, A18, A19, Th22; :: thesis: verum