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 W be Subset of (Segre_Product A); :: thesis:
assume A2: ( not W is trivial & W is strong & W is closed_under_lines ) ; :: thesis:
consider K being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A3: W = product K and
A4: for S being Subset of (A . (indx K)) st S = K . (indx K) holds
( S is strong & S is closed_under_lines ) by A2, PENCIL_1:29;
set O = [#] (A . (indx K));
set 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 ) } ;
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 ) } c= the carrier of (Segre_Product A)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in 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:
then consider y being set such that
A5: a in y and
A6: y in { 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 ) } by TARSKI:def 4;
ex Y being Subset of (Segre_Product A) st
( y = Y & not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) by A6;
hence a in the carrier of (Segre_Product A) by A5; :: thesis:

end;

then reconsider C = 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 ) } as Subset of (Segre_Product A) ;
dom A = I by PARTFUN1:def 2;
then A . (indx K) in rng A by FUNCT_1:3;
then A7: not A . (indx K) is trivial by PENCIL_1:def 17;
then reconsider L = K +* ((indx K),([#] (A . (indx K)))) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by Th7, PENCIL_1:27;
dom K = I by PARTFUN1:def 2;
then L . (indx K) = [#] (A . (indx K)) by FUNCT_7:31;
then A8: indx K = indx L by A7, PENCIL_1:def 21;
A9: product L c= C

proof

K c= Carrier A by PBOOLE:def 18;
then K . (indx K) c= (Carrier A) . (indx K) ;
then reconsider S = K . (indx K) as Subset of (A . (indx K)) by YELLOW_6:2;
let y be object ; :: according to TARSKI:def 3 :: thesis:
A10: dom K = I by PARTFUN1:def 2;
A11: A . (indx K) is strongly_connected by A1;
assume y in product L ; :: thesis:
then consider z being Function such that
A12: z = y and
A13: dom z = dom L and
A14: for a being object st a in dom L holds
z . a in L . a by CARD_3:def 5;
A15: dom L = I by PARTFUN1:def 2;
then reconsider z = z as ManySortedSet of I by A13, PARTFUN1:def 2, RELAT_1:def 18;
z . (indx K) in L . (indx K) by A14, A15;
then reconsider zi = z . (indx K) as Point of (A . (indx K)) by A10, FUNCT_7:31;
( not S is trivial & S is strong & S is closed_under_lines ) by A4, PENCIL_1:def 21;
then consider f being FinSequence of bool the carrier of (A . (indx K)) such that
A16: S = f . 1 and
A17: zi in f . (len f) and
A18: for Z being Subset of (A . (indx K)) st Z in rng f holds
( Z is closed_under_lines & Z is strong ) and
A19: for i being Nat st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) by A11;
A20: len f in dom f by A17, FUNCT_1:def 2;
then 1 in dom f by FINSEQ_5:6, RELAT_1:38;
then A21: 1 in Seg (len f) by FINSEQ_1:def 3;
A22: not f . (len f) is trivial

proof

reconsider l1 = (len f) - 1 as Element of NAT by A20, FINSEQ_3:26;
A23: 1 <= len f by A20, FINSEQ_3:25;

per cases by A23, XXREAL_0:1;

suppose len f = 1 ; :: thesis:

hence not f . (len f) is trivial by A16, PENCIL_1:def 21; :: thesis:

end;

suppose len f > 1 ; :: thesis:

then 1 + 1 <= len f by NAT_1:13;
then A24: 2 - 1 <= l1 by XREAL_1:9;
A25: card ((f . l1) /\ (f . (l1 + 1))) c= card (f . (l1 + 1)) by CARD_1:11, XBOOLE_1:17;
l1 < (len f) - 0 by XREAL_1:15;
then 2 c= card ((f . l1) /\ (f . (l1 + 1))) by A19, A24;
then 2 c= card (f . (l1 + 1)) by A25;
hence not f . (len f) is trivial by PENCIL_1:4; :: thesis:

end;

then reconsider ff = f . (len f) as non trivial set ;
L . (indx K) = [#] (A . (indx K)) by A10, FUNCT_7:31;
then indx K = indx L by A7, PENCIL_1:def 21;
then reconsider EL = L +* ((indx K),ff) as non trivial-yielding Segre-like ManySortedSet of I by PENCIL_1:27;
A26: dom z = dom (L +* ((indx K),(f . (len f)))) by A13, FUNCT_7:30;
deffunc H₁( set ) -> set = product (L +* ((indx K),(f . $1)));
consider g being FinSequence such that
A27: ( len g = len f & ( for k being Nat st k in dom g holds
g . k = H₁(k) ) ) from FINSEQ_1:sch 2();
A28: rng g c= bool the carrier of (Segre_Product A)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
reconsider aa = a as set by TARSKI:1;
A29: dom (Carrier A) = I by PARTFUN1:def 2;
assume a in rng g ; :: thesis:
then consider k being object such that
A30: k in dom g and
A31: a = g . k by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A30;
A32: k in Seg (len f) by A27, A30, FINSEQ_1:def 3;

A33: now :: thesis:

let o be object ; :: thesis:
assume A34: o in I ; :: thesis:
A35: k in dom f by A32, FINSEQ_1:def 3;

per cases ;

suppose A36: o <> indx K ; :: thesis:

then (L +* ((indx K),(f . k))) . o = L . o by FUNCT_7:32;
then A37: (L +* ((indx K),(f . k))) . o = K . o by A36, FUNCT_7:32;
K c= Carrier A by PBOOLE:def 18;
hence (L +* ((indx K),(f . k))) . o c= (Carrier A) . o by A34, A37; :: thesis:

end;

suppose A38: o = indx K ; :: thesis:

then (L +* ((indx K),(f . k))) . o = f . k by A15, FUNCT_7:31;
then (L +* ((indx K),(f . k))) . o in rng f by A35, FUNCT_1:3;
then (L +* ((indx K),(f . k))) . o c= the carrier of (A . (indx K)) ;
hence (L +* ((indx K),(f . k))) . o c= (Carrier A) . o by A38, YELLOW_6:2; :: thesis:

end;

dom (L +* ((indx K),(f . k))) = I by PARTFUN1:def 2;
then product (L +* ((indx K),(f . k))) c= product (Carrier A) by A29, A33, CARD_3:27;
then aa c= product (Carrier A) by A27, A30, A31;
hence a in bool the carrier of (Segre_Product A) ; :: thesis:

end;

A39: dom g = Seg (len f) by A27, FINSEQ_1:def 3;
reconsider g = g as FinSequence of bool the carrier of (Segre_Product A) by A28, FINSEQ_1:def 4;
len f in dom g by A20, A27, FINSEQ_3:29;
then A40: g . (len f) in rng g by FUNCT_1:3;
then reconsider Yb = g . (len f) as Subset of (Segre_Product A) ;

A41: now :: thesis:

let o be object ; :: thesis:
assume o in I ; :: thesis:

per cases ;

suppose A42: o <> indx K ; :: thesis:

then (L +* ((indx K),(f . 1))) . o = L . o by FUNCT_7:32;
hence (L +* ((indx K),(f . 1))) . o = K . o by A42, FUNCT_7:32; :: thesis:

end;

suppose o = indx K ; :: thesis:

hence (L +* ((indx K),(f . 1))) . o = K . o by A15, A16, FUNCT_7:31; :: thesis:

end;

A43: for V being Subset of (Segre_Product A) st V in rng g holds
( V is closed_under_lines & V is strong )

proof

let V be Subset of (Segre_Product A); :: thesis:
assume V in rng g ; :: thesis:
then consider n1 being object such that
A44: n1 in dom g and
A45: V = g . n1 by FUNCT_1:def 3;
reconsider n = n1 as Element of NAT by A44;
n in Seg (len f) by A27, A44, FINSEQ_1:def 3;
then A46: n in dom f by FINSEQ_1:def 3;
not f . n is trivial

proof

A47: n <= len f by A46, FINSEQ_3:25;

per cases by A46, A47, FINSEQ_3:25, XXREAL_0:1;

suppose ( 1 <= n & n = len f ) ; :: thesis:

hence not f . n is trivial by A22; :: thesis:

end;

suppose A48: ( 1 <= n & n < len f ) ; :: thesis:

A49: card ((f . n) /\ (f . (n + 1))) c= card (f . n) by CARD_1:11, XBOOLE_1:17;
2 c= card ((f . n) /\ (f . (n + 1))) by A19, A48;
then 2 c= card (f . n) by A49;
hence not f . n is trivial by PENCIL_1:4; :: thesis:

end;

then reconsider fn = f . n as non trivial set ;
A50: L +* ((indx K),(f . n)) c= Carrier A

proof

let o be object ; :: according to PBOOLE:def 2 :: thesis:
assume A51: o in I ; :: thesis:

per cases ;

suppose A52: o <> indx K ; :: thesis:

A53: L c= Carrier A by PBOOLE:def 18;
(L +* ((indx K),(f . n))) . o = L . o by A52, FUNCT_7:32;
hence (L +* ((indx K),(f . n))) . o c= (Carrier A) . o by A51, A53; :: thesis:

end;

suppose A54: o = indx K ; :: thesis:

then (L +* ((indx K),(f . n))) . o = f . n by A15, FUNCT_7:31;
then (L +* ((indx K),(f . n))) . o in rng f by A46, FUNCT_1:3;
then (L +* ((indx K),(f . n))) . o c= the carrier of (A . (indx K)) ;
hence (L +* ((indx K),(f . n))) . o c= (Carrier A) . o by A54, YELLOW_6:2; :: thesis:

end;

L . (indx K) = [#] (A . (indx K)) by A10, FUNCT_7:31;
then indx K = indx L by A7, PENCIL_1:def 21;
then reconsider LI = L +* ((indx K),fn) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A50, PBOOLE:def 18, PENCIL_1:27;
reconsider LI = LI as non trivial-yielding Segre-like ManySortedSubset of Carrier A ;
A55: LI . (indx K) = fn by A15, FUNCT_7:31;
then A56: indx LI = indx K by PENCIL_1:def 21;

A57: now :: thesis:

let D be Subset of (A . (indx LI)); :: thesis:
assume D = LI . (indx LI) ; :: thesis:
then D in rng f by A46, A55, A56, FUNCT_1:3;
hence ( D is strong & D is closed_under_lines ) by A18, A56; :: thesis:

end;

g . n = product (L +* ((indx K),(f . n))) by A27, A44;
hence ( V is closed_under_lines & V is strong ) by A45, A57, PENCIL_1:29; :: thesis:

end;

A58: len f in Seg (len f) by A20, FINSEQ_1:def 3;
then Yb = product EL by A27, A39;
then A59: ( not Yb is trivial & Yb is strong & Yb is closed_under_lines ) by A40, A43;
A60: for i being Element of NAT st 1 <= i & i < len g holds
2 c= card ((g . i) /\ (g . (i + 1)))

proof

consider l1 being object such that
A61: l1 in product L by XBOOLE_0:def 1;
let i be Element of NAT ; :: thesis:
assume that
A62: 1 <= i and
A63: i < len g ; :: thesis:
i in Seg (len f) by A27, A62, A63, FINSEQ_1:1;
then A64: g . i = product (L +* ((indx K),(f . i))) by A27, A39;
2 c= card ((f . i) /\ (f . (i + 1))) by A19, A27, A62, A63;
then consider a, b being object such that
A65: a in (f . i) /\ (f . (i + 1)) and
A66: b in (f . i) /\ (f . (i + 1)) and
A67: a <> b by PENCIL_1:2;
consider l being Function such that
l = l1 and
A68: dom l = dom L and
A69: for o being object st o in dom L holds
l . o in L . o by A61, CARD_3:def 5;
reconsider l = l as ManySortedSet of I by A15, A68, PARTFUN1:def 2, RELAT_1:def 18;
set l1 = l +* ((indx K),a);
set l2 = l +* ((indx K),b);
A70: i + 1 <= len g by A63, NAT_1:13;

A71: now :: thesis:

let o be object ; :: thesis:
assume o in dom (L +* ((indx K),(f . i))) ; :: thesis:
then A72: o in I ;
then A73: o in dom l by PARTFUN1:def 2;

per cases ;

suppose A74: o = indx K ; :: thesis:

then (l +* ((indx K),a)) . o = a by A73, FUNCT_7:31;
then (l +* ((indx K),a)) . o in f . i by A65, XBOOLE_0:def 4;
hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . i))) . o by A15, A74, FUNCT_7:31; :: thesis:

end;

suppose A75: o <> indx K ; :: thesis:

then A76: (l +* ((indx K),a)) . o = l . o by FUNCT_7:32;
l . o in L . o by A15, A69, A72;
hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . i))) . o by A75, A76, FUNCT_7:32; :: thesis:

end;

1 <= i + 1 by A62, NAT_1:13;
then i + 1 in Seg (len f) by A27, A70, FINSEQ_1:1;
then A77: g . (i + 1) = product (L +* ((indx K),(f . (i + 1)))) by A27, A39;

A78: now :: thesis:

let o be object ; :: thesis:
assume o in dom (L +* ((indx K),(f . i))) ; :: thesis:
then A79: o in I ;
then A80: o in dom l by PARTFUN1:def 2;

per cases ;

suppose A81: o = indx K ; :: thesis:

then (l +* ((indx K),b)) . o = b by A80, FUNCT_7:31;
then (l +* ((indx K),b)) . o in f . i by A66, XBOOLE_0:def 4;
hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . i))) . o by A15, A81, FUNCT_7:31; :: thesis:

end;

suppose A82: o <> indx K ; :: thesis:

then A83: (l +* ((indx K),b)) . o = l . o by FUNCT_7:32;
l . o in L . o by A15, A69, A79;
hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . i))) . o by A82, A83, FUNCT_7:32; :: thesis:

end;

A84: now :: thesis:

let o be object ; :: thesis:
assume o in dom (L +* ((indx K),(f . (i + 1)))) ; :: thesis:
then A85: o in I ;
then A86: o in dom l by PARTFUN1:def 2;

per cases ;

suppose A87: o = indx K ; :: thesis:

then (l +* ((indx K),a)) . o = a by A86, FUNCT_7:31;
then (l +* ((indx K),a)) . o in f . (i + 1) by A65, XBOOLE_0:def 4;
hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . (i + 1)))) . o by A15, A87, FUNCT_7:31; :: thesis:

end;

suppose A88: o <> indx K ; :: thesis:

then A89: (l +* ((indx K),a)) . o = l . o by FUNCT_7:32;
l . o in L . o by A15, A69, A85;
hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . (i + 1)))) . o by A88, A89, FUNCT_7:32; :: thesis:

end;

dom (l +* ((indx K),a)) = I by PARTFUN1:def 2
.= dom (L +* ((indx K),(f . (i + 1)))) by PARTFUN1:def 2 ;
then A90: l +* ((indx K),a) in product (L +* ((indx K),(f . (i + 1)))) by A84, CARD_3:9;

A91: now :: thesis:

let o be object ; :: thesis:
assume o in dom (L +* ((indx K),(f . (i + 1)))) ; :: thesis:
then A92: o in I ;
then A93: o in dom l by PARTFUN1:def 2;

per cases ;

suppose A94: o = indx K ; :: thesis:

then (l +* ((indx K),b)) . o = b by A93, FUNCT_7:31;
then (l +* ((indx K),b)) . o in f . (i + 1) by A66, XBOOLE_0:def 4;
hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . (i + 1)))) . o by A15, A94, FUNCT_7:31; :: thesis:

end;

suppose A95: o <> indx K ; :: thesis:

then A96: (l +* ((indx K),b)) . o = l . o by FUNCT_7:32;
l . o in L . o by A15, A69, A92;
hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . (i + 1)))) . o by A95, A96, FUNCT_7:32; :: thesis:

end;

dom (l +* ((indx K),b)) = I by PARTFUN1:def 2
.= dom (L +* ((indx K),(f . (i + 1)))) by PARTFUN1:def 2 ;
then A97: l +* ((indx K),b) in product (L +* ((indx K),(f . (i + 1)))) by A91, CARD_3:9;
dom (l +* ((indx K),b)) = I by PARTFUN1:def 2
.= dom (L +* ((indx K),(f . i))) by PARTFUN1:def 2 ;
then l +* ((indx K),b) in product (L +* ((indx K),(f . i))) by A78, CARD_3:9;
then A98: l +* ((indx K),b) in (g . i) /\ (g . (i + 1)) by A64, A77, A97, XBOOLE_0:def 4;
(l +* ((indx K),a)) . (indx K) = a by A15, A68, FUNCT_7:31;
then A99: l +* ((indx K),a) <> l +* ((indx K),b) by A15, A67, A68, FUNCT_7:31;
dom (l +* ((indx K),a)) = I by PARTFUN1:def 2
.= dom (L +* ((indx K),(f . i))) by PARTFUN1:def 2 ;
then l +* ((indx K),a) in product (L +* ((indx K),(f . i))) by A71, CARD_3:9;
then l +* ((indx K),a) in (g . i) /\ (g . (i + 1)) by A64, A77, A90, XBOOLE_0:def 4;
hence 2 c= card ((g . i) /\ (g . (i + 1))) by A99, A98, PENCIL_1:2; :: thesis:

end;

A100: now :: thesis:

let o be object ; :: thesis:
assume o in dom (L +* ((indx K),(f . (len f)))) ; :: thesis:
then A101: o in I ;

per cases ;

suppose o = indx K ; :: thesis:

hence z . o in (L +* ((indx K),(f . (len f)))) . o by A15, A17, FUNCT_7:31; :: thesis:

end;

suppose A102: o <> indx K ; :: thesis:

z . o in L . o by A14, A15, A101;
hence z . o in (L +* ((indx K),(f . (len f)))) . o by A102, FUNCT_7:32; :: thesis:

end;

L +* ((indx K),(f . 1)) = K by A41;
then W = g . 1 by A3, A27, A39, A21;
then W,Yb are_joinable by A27, A43, A60;
then A103: Yb in { 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 ) } by A59;
Yb = product (L +* ((indx K),(f . (len f)))) by A27, A39, A58;
then y in Yb by A12, A26, A100, CARD_3:9;
hence y in C by A103, TARSKI:def 4; :: thesis:

end;

dom K = I by PARTFUN1:def 2;
then A104: L . (indx L) = [#] (A . (indx L)) by A8, FUNCT_7:31;
C c= product L

proof

let c be object ; :: according to TARSKI:def 3 :: thesis:
assume c in C ; :: thesis:
then consider y being set such that
A105: c in y and
A106: y in { 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 ) } by TARSKI:def 4;
consider Y being Subset of (Segre_Product A) such that
A107: y = Y and
A108: ( not Y is trivial & Y is strong & Y is closed_under_lines ) and
A109: W,Y are_joinable by A106;
reconsider c1 = c as ManySortedSet of I by A105, A107, PENCIL_1:14;
consider M being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A110: Y = product M and
for S being Subset of (A . (indx M)) st S = M . (indx M) holds
( S is strong & S is closed_under_lines ) by A108, PENCIL_1:29;
A111: dom M = I by PARTFUN1:def 2
.= dom L by PARTFUN1:def 2 ;
A112: dom K = I by PARTFUN1:def 2
.= dom L by PARTFUN1:def 2 ;
A113: for a being object st a in dom L holds
c1 . a in L . a

proof

let a be object ; :: thesis:
assume A114: a in dom L ; :: thesis:
then reconsider a1 = a as Element of I ;

per cases ;

suppose A115: a = indx K ; :: thesis:

M c= Carrier A by PBOOLE:def 18;
then M . a1 c= (Carrier A) . a1 ;
then A116: M . a1 c= the carrier of (A . a1) by YELLOW_6:2;
c1 . a in M . a by A105, A107, A110, A111, A114, CARD_3:9;
then c1 . a in [#] (A . (indx K)) by A115, A116;
hence c1 . a in L . a by A112, A114, A115, FUNCT_7:31; :: thesis:

end;

suppose A117: a <> indx K ; :: thesis:

c1 . a in M . a by A105, A107, A110, A111, A114, CARD_3:9;
then c1 . a in K . a by A2, A3, A108, A109, A110, A117, Th11;
hence c1 . a in L . a by A117, FUNCT_7:32; :: thesis:

end;

dom c1 = I by PARTFUN1:def 2
.= dom L by PARTFUN1:def 2 ;
hence c in product L by A113, CARD_3:9; :: thesis:

end;

then C = product L by A9;
hence 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 ) } is Segre-Coset of A by A104, Def2; :: thesis: