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 W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds

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

let A be PLS-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds

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 )

assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis: for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds

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

let W be Subset of (Segre_Product A); :: thesis: ( not W is trivial & W is strong & W is closed_under_lines implies 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 )

assume A2: ( not W is trivial & W is strong & W is closed_under_lines ) ; :: thesis: 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

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)

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

then A104: L . (indx L) = [#] (A . (indx L)) by A8, FUNCT_7:31;

C c= product L

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

for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds

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

let A be PLS-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds

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 )

assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis: for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds

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

let W be Subset of (Segre_Product A); :: thesis: ( not W is trivial & W is strong & W is closed_under_lines implies 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 )

assume A2: ( not W is trivial & W is strong & W is closed_under_lines ) ; :: thesis: 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

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

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) ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not 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 ) } or a in the carrier of (Segre_Product A) )

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: a in the carrier of (Segre_Product A)

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

end;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: a in the carrier of (Segre_Product A)

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

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

dom K = I
by PARTFUN1:def 2;
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: ( not y in product L or y in C )

A10: dom K = I by PARTFUN1:def 2;

A11: A . (indx K) is strongly_connected by A1;

assume y in product L ; :: thesis: y in C

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

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_{1}( 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_{1}(k) ) )
from FINSEQ_1:sch 2();

A28: rng g c= bool the carrier of (Segre_Product A)

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) ;

( V is closed_under_lines & V is strong )

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

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

end;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: ( not y in product L or y in C )

A10: dom K = I by PARTFUN1:def 2;

A11: A . (indx K) is strongly_connected by A1;

assume y in product L ; :: thesis: y in C

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

then reconsider ff = f . (len f) as non trivial set ;
reconsider l1 = (len f) - 1 as Element of NAT by A20, FINSEQ_3:26;

A23: 1 <= len f by A20, FINSEQ_3:25;

end;A23: 1 <= len f by A20, FINSEQ_3:25;

per cases
( len f = 1 or len f > 1 )
by A23, XXREAL_0:1;

end;

suppose
len f > 1
; :: thesis: not f . (len f) is trivial

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

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

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

consider g being FinSequence such that

A27: ( len g = len f & ( for k being Nat st k in dom g holds

g . k = H

A28: rng g c= bool the carrier of (Segre_Product A)

proof

A39:
dom g = Seg (len f)
by A27, FINSEQ_1:def 3;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng g or a in bool the carrier of (Segre_Product A) )

reconsider aa = a as set by TARSKI:1;

A29: dom (Carrier A) = I by PARTFUN1:def 2;

assume a in rng g ; :: thesis: a in bool the carrier of (Segre_Product A)

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;

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

end;reconsider aa = a as set by TARSKI:1;

A29: dom (Carrier A) = I by PARTFUN1:def 2;

assume a in rng g ; :: thesis: a in bool the carrier of (Segre_Product A)

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: for o being object st o in I holds

(L +* ((indx K),(f . k))) . o c= (Carrier A) . o

dom (L +* ((indx K),(f . k))) = I
by PARTFUN1:def 2;(L +* ((indx K),(f . k))) . o c= (Carrier A) . o

let o be object ; :: thesis: ( o in I implies (L +* ((indx K),(f . k))) . b_{1} c= (Carrier A) . b_{1} )

assume A34: o in I ; :: thesis: (L +* ((indx K),(f . k))) . b_{1} c= (Carrier A) . b_{1}

A35: k in dom f by A32, FINSEQ_1:def 3;

end;assume A34: o in I ; :: thesis: (L +* ((indx K),(f . k))) . b

A35: k in dom f by A32, FINSEQ_1:def 3;

per cases
( o <> indx K or o = indx K )
;

end;

suppose A36:
o <> indx K
; :: thesis: (L +* ((indx K),(f . k))) . b_{1} c= (Carrier A) . b_{1}

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

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

suppose A38:
o = indx K
; :: thesis: (L +* ((indx K),(f . k))) . b_{1} c= (Carrier A) . b_{1}

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

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

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

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: for o being object st o in I holds

(L +* ((indx K),(f . 1))) . o = K . o

A43:
for V being Subset of (Segre_Product A) st V in rng g holds (L +* ((indx K),(f . 1))) . o = K . o

let o be object ; :: thesis: ( o in I implies (L +* ((indx K),(f . 1))) . b_{1} = K . b_{1} )

assume o in I ; :: thesis: (L +* ((indx K),(f . 1))) . b_{1} = K . b_{1}

end;assume o in I ; :: thesis: (L +* ((indx K),(f . 1))) . b

( V is closed_under_lines & V is strong )

proof

A58:
len f in Seg (len f)
by A20, FINSEQ_1:def 3;
let V be Subset of (Segre_Product A); :: thesis: ( V in rng g implies ( V is closed_under_lines & V is strong ) )

assume V in rng g ; :: thesis: ( V is closed_under_lines & V is strong )

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

A50: L +* ((indx K),(f . n)) c= Carrier A

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;

hence ( V is closed_under_lines & V is strong ) by A45, A57, PENCIL_1:29; :: thesis: verum

end;assume V in rng g ; :: thesis: ( V is closed_under_lines & V is strong )

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

then reconsider fn = f . n as non trivial set ;
A47:
n <= len f
by A46, FINSEQ_3:25;

end;A50: L +* ((indx K),(f . n)) c= Carrier A

proof

L . (indx K) = [#] (A . (indx K))
by A10, FUNCT_7:31;
let o be object ; :: according to PBOOLE:def 2 :: thesis: ( not o in I or (L +* ((indx K),(f . n))) . o c= (Carrier A) . o )

assume A51: o in I ; :: thesis: (L +* ((indx K),(f . n))) . o c= (Carrier A) . o

end;assume A51: o in I ; :: thesis: (L +* ((indx K),(f . n))) . o c= (Carrier A) . o

per cases
( o <> indx K or o = indx K )
;

end;

suppose A52:
o <> indx K
; :: thesis: (L +* ((indx K),(f . n))) . o c= (Carrier A) . o

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

end;(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: verum

suppose A54:
o = indx K
; :: thesis: (L +* ((indx K),(f . n))) . o c= (Carrier A) . o

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

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

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: for D being Subset of (A . (indx LI)) st D = LI . (indx LI) holds

( D is strong & D is closed_under_lines )

g . n = product (L +* ((indx K),(f . n)))
by A27, A44;( D is strong & D is closed_under_lines )

let D be Subset of (A . (indx LI)); :: thesis: ( D = LI . (indx LI) implies ( D is strong & D is closed_under_lines ) )

assume D = LI . (indx LI) ; :: thesis: ( D is strong & D is closed_under_lines )

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

end;assume D = LI . (indx LI) ; :: thesis: ( D is strong & D is closed_under_lines )

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

hence ( V is closed_under_lines & V is strong ) by A45, A57, PENCIL_1:29; :: thesis: verum

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: ( 1 <= i & i < len g implies 2 c= card ((g . i) /\ (g . (i + 1))) )

assume that

A62: 1 <= i and

A63: i < len g ; :: thesis: 2 c= card ((g . i) /\ (g . (i + 1)))

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;

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;

.= 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;

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

end;A61: l1 in product L by XBOOLE_0:def 1;

let i be Element of NAT ; :: thesis: ( 1 <= i & i < len g implies 2 c= card ((g . i) /\ (g . (i + 1))) )

assume that

A62: 1 <= i and

A63: i < len g ; :: thesis: 2 c= card ((g . i) /\ (g . (i + 1)))

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: for o being object st o in dom (L +* ((indx K),(f . i))) holds

(l +* ((indx K),a)) . o in (L +* ((indx K),(f . i))) . o

1 <= i + 1
by A62, NAT_1:13;(l +* ((indx K),a)) . o in (L +* ((indx K),(f . i))) . o

let o be object ; :: thesis: ( o in dom (L +* ((indx K),(f . i))) implies (l +* ((indx K),a)) . b_{1} in (L +* ((indx K),(f . i))) . b_{1} )

assume o in dom (L +* ((indx K),(f . i))) ; :: thesis: (l +* ((indx K),a)) . b_{1} in (L +* ((indx K),(f . i))) . b_{1}

then A72: o in I ;

then A73: o in dom l by PARTFUN1:def 2;

end;assume o in dom (L +* ((indx K),(f . i))) ; :: thesis: (l +* ((indx K),a)) . b

then A72: o in I ;

then A73: o in dom l by PARTFUN1:def 2;

per cases
( o = indx K or o <> indx K )
;

end;

suppose A74:
o = indx K
; :: thesis: (l +* ((indx K),a)) . b_{1} in (L +* ((indx K),(f . i))) . b_{1}

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

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

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: for o being object st o in dom (L +* ((indx K),(f . i))) holds

(l +* ((indx K),b)) . o in (L +* ((indx K),(f . i))) . o

(l +* ((indx K),b)) . o in (L +* ((indx K),(f . i))) . o

let o be object ; :: thesis: ( o in dom (L +* ((indx K),(f . i))) implies (l +* ((indx K),b)) . b_{1} in (L +* ((indx K),(f . i))) . b_{1} )

assume o in dom (L +* ((indx K),(f . i))) ; :: thesis: (l +* ((indx K),b)) . b_{1} in (L +* ((indx K),(f . i))) . b_{1}

then A79: o in I ;

then A80: o in dom l by PARTFUN1:def 2;

end;assume o in dom (L +* ((indx K),(f . i))) ; :: thesis: (l +* ((indx K),b)) . b

then A79: o in I ;

then A80: o in dom l by PARTFUN1:def 2;

per cases
( o = indx K or o <> indx K )
;

end;

suppose A81:
o = indx K
; :: thesis: (l +* ((indx K),b)) . b_{1} in (L +* ((indx K),(f . i))) . b_{1}

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

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

A84: now :: thesis: for o being object st o in dom (L +* ((indx K),(f . (i + 1)))) holds

(l +* ((indx K),a)) . o in (L +* ((indx K),(f . (i + 1)))) . o

dom (l +* ((indx K),a)) =
I
by PARTFUN1:def 2
(l +* ((indx K),a)) . o in (L +* ((indx K),(f . (i + 1)))) . o

let o be object ; :: thesis: ( o in dom (L +* ((indx K),(f . (i + 1)))) implies (l +* ((indx K),a)) . b_{1} in (L +* ((indx K),(f . (i + 1)))) . b_{1} )

assume o in dom (L +* ((indx K),(f . (i + 1)))) ; :: thesis: (l +* ((indx K),a)) . b_{1} in (L +* ((indx K),(f . (i + 1)))) . b_{1}

then A85: o in I ;

then A86: o in dom l by PARTFUN1:def 2;

end;assume o in dom (L +* ((indx K),(f . (i + 1)))) ; :: thesis: (l +* ((indx K),a)) . b

then A85: o in I ;

then A86: o in dom l by PARTFUN1:def 2;

per cases
( o = indx K or o <> indx K )
;

end;

suppose A87:
o = indx K
; :: thesis: (l +* ((indx K),a)) . b_{1} in (L +* ((indx K),(f . (i + 1)))) . b_{1}

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

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

suppose A88:
o <> indx K
; :: thesis: (l +* ((indx K),a)) . b_{1} in (L +* ((indx K),(f . (i + 1)))) . b_{1}

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

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

.= 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: for o being object st o in dom (L +* ((indx K),(f . (i + 1)))) holds

(l +* ((indx K),b)) . o in (L +* ((indx K),(f . (i + 1)))) . o

dom (l +* ((indx K),b)) =
I
by PARTFUN1:def 2
(l +* ((indx K),b)) . o in (L +* ((indx K),(f . (i + 1)))) . o

let o be object ; :: thesis: ( o in dom (L +* ((indx K),(f . (i + 1)))) implies (l +* ((indx K),b)) . b_{1} in (L +* ((indx K),(f . (i + 1)))) . b_{1} )

assume o in dom (L +* ((indx K),(f . (i + 1)))) ; :: thesis: (l +* ((indx K),b)) . b_{1} in (L +* ((indx K),(f . (i + 1)))) . b_{1}

then A92: o in I ;

then A93: o in dom l by PARTFUN1:def 2;

end;assume o in dom (L +* ((indx K),(f . (i + 1)))) ; :: thesis: (l +* ((indx K),b)) . b

then A92: o in I ;

then A93: o in dom l by PARTFUN1:def 2;

per cases
( o = indx K or o <> indx K )
;

end;

suppose A94:
o = indx K
; :: thesis: (l +* ((indx K),b)) . b_{1} in (L +* ((indx K),(f . (i + 1)))) . b_{1}

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

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

suppose A95:
o <> indx K
; :: thesis: (l +* ((indx K),b)) . b_{1} in (L +* ((indx K),(f . (i + 1)))) . b_{1}

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

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

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

A100: now :: thesis: for o being object st o in dom (L +* ((indx K),(f . (len f)))) holds

z . o in (L +* ((indx K),(f . (len f)))) . o

L +* ((indx K),(f . 1)) = K
by A41;z . o in (L +* ((indx K),(f . (len f)))) . o

let o be object ; :: thesis: ( o in dom (L +* ((indx K),(f . (len f)))) implies z . b_{1} in (L +* ((indx K),(f . (len f)))) . b_{1} )

assume o in dom (L +* ((indx K),(f . (len f)))) ; :: thesis: z . b_{1} in (L +* ((indx K),(f . (len f)))) . b_{1}

then A101: o in I ;

end;assume o in dom (L +* ((indx K),(f . (len f)))) ; :: thesis: z . b

then A101: o in I ;

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

then A104: L . (indx L) = [#] (A . (indx L)) by A8, FUNCT_7:31;

C c= product L

proof

then
C = product L
by A9;
let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in C or c in product L )

assume c in C ; :: thesis: c in product L

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

.= dom L by PARTFUN1:def 2 ;

hence c in product L by A113, CARD_3:9; :: thesis: verum

end;assume c in C ; :: thesis: c in product L

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

dom c1 =
I
by PARTFUN1:def 2
let a be object ; :: thesis: ( a in dom L implies c1 . a in L . a )

assume A114: a in dom L ; :: thesis: c1 . a in L . a

then reconsider a1 = a as Element of I ;

end;assume A114: a in dom L ; :: thesis: c1 . a in L . a

then reconsider a1 = a as Element of I ;

per cases
( a = indx K or a <> indx K )
;

end;

suppose A115:
a = indx K
; :: thesis: c1 . a in L . a

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

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

.= dom L by PARTFUN1:def 2 ;

hence c in product L by A113, CARD_3:9; :: thesis: verum

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