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 (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 ) } ) )

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 (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 ) } ) ) )

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 (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 ) } ) )

let B be set ; :: thesis: ( B is Segre-Coset of A iff 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 ) } ) )

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: ( 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 ) } ) implies B is Segre-Coset of A )

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: B is Segre-Coset of A

thus B is Segre-Coset of A by A1, A18, A19, Th22; :: thesis: verum

for B being set holds

( B is Segre-Coset of A iff 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 ) } ) )

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 (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 ) } ) ) )

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 (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 ) } ) )

let B be set ; :: thesis: ( B is Segre-Coset of A iff 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 ) } ) )

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: ( 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 ) } ) implies B is Segre-Coset of A )

proof

given W being Subset of (Segre_Product A) such that A18:
( not W is trivial & W is strong & W is closed_under_lines )
and
assume
B is Segre-Coset of A
; :: thesis: 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 ) } )

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

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

then reconsider psX = pX as Subset of (Segre_Product A) ;

take psX ; :: thesis: ( not psX is trivial & psX is strong & psX 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 & psX,Y are_joinable ) } )

thus A14: ( not psX is trivial & psX is strong & psX is closed_under_lines ) by PENCIL_1:20, PENCIL_1:21; :: thesis: 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 ) }

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: verum

end;( 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 ) } )

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

proof

then reconsider V = V as Element of Carrier A by PBOOLE:def 14;
let i be object ; :: thesis: ( i in I implies V . i is Element of (Carrier A) . i )

assume A7: i in I ; :: thesis: V . i is Element of (Carrier A) . i

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: verum

end;assume A7: i in I ; :: thesis: V . i is Element of (Carrier A) . i

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: verum

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

proof

pX in the topology of (Segre_Product A)
;
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

end;assume A12: i in I ; :: thesis: X . i c= L . i

then reconsider psX = pX as Subset of (Segre_Product A) ;

take psX ; :: thesis: ( not psX is trivial & psX is strong & psX 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 & psX,Y are_joinable ) } )

thus A14: ( not psX is trivial & psX is strong & psX is closed_under_lines ) by PENCIL_1:20, PENCIL_1:21; :: thesis: 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 ) }

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: verum

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: B is Segre-Coset of A

thus B is Segre-Coset of A by A1, A18, A19, Th22; :: thesis: verum