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 () st not W is trivial & W is strong & W is closed_under_lines holds
union { Y where Y is Subset of () : ( 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 () st not W is trivial & W is strong & W is closed_under_lines holds
union { Y where Y is Subset of () : ( 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 () st not W is trivial & W is strong & W is closed_under_lines holds
union { Y where Y is Subset of () : ( 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 (); :: thesis: ( not W is trivial & W is strong & W is closed_under_lines implies union { Y where Y is Subset of () : ( 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 () : ( 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 ;
set O = [#] (A . (indx K));
set B = union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ;
union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } c= the carrier of ()
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } or a in the carrier of () )
assume a in union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ; :: thesis: a in the carrier of ()
then consider y being set such that
A5: a in y and
A6: y in { Y where Y is Subset of () : ( 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 () 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 () by A5; :: thesis: verum
end;
then reconsider C = union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } as Subset of () ;
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 ;
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 ;
A9: product L c= C
proof
K c= Carrier A by PBOOLE:def 18;
then K . (indx K) c= () . (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 ;
z . (indx K) in L . (indx K) by ;
then reconsider zi = z . (indx K) as Point of (A . (indx K)) by ;
( not S is trivial & S is strong & S is closed_under_lines ) by ;
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 ;
then 1 in dom f by ;
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 ;
A23: 1 <= len f by ;
per cases ( len f = 1 or len f > 1 ) by ;
suppose len f = 1 ; :: thesis: not f . (len f) is trivial
hence not f . (len f) is trivial by ; :: thesis: verum
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 ;
l1 < (len f) - 0 by XREAL_1:15;
then 2 c= card ((f . l1) /\ (f . (l1 + 1))) by ;
then 2 c= card (f . (l1 + 1)) by A25;
hence not f . (len f) is trivial by PENCIL_1:4; :: thesis: verum
end;
end;
end;
then reconsider ff = f . (len f) as non trivial set ;
L . (indx K) = [#] (A . (indx K)) by ;
then indx K = indx L by ;
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 ;
deffunc H1( 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 = H1(k) ) ) from A28: rng g c= bool the carrier of ()
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng g or a in bool the carrier of () )
reconsider aa = a as set by TARSKI:1;
A29: dom () = I by PARTFUN1:def 2;
assume a in rng g ; :: thesis: a in bool the carrier of ()
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 ;
A33: now :: thesis: for o being object st o in I holds
(L +* ((indx K),(f . k))) . o c= () . o
let o be object ; :: thesis: ( o in I implies (L +* ((indx K),(f . k))) . b1 c= () . b1 )
assume A34: o in I ; :: thesis: (L +* ((indx K),(f . k))) . b1 c= () . b1
A35: k in dom f by ;
per cases ( o <> indx K or o = indx K ) ;
suppose A36: o <> indx K ; :: thesis: (L +* ((indx K),(f . k))) . b1 c= () . b1
then (L +* ((indx K),(f . k))) . o = L . o by FUNCT_7:32;
then A37: (L +* ((indx K),(f . k))) . o = K . o by ;
K c= Carrier A by PBOOLE:def 18;
hence (L +* ((indx K),(f . k))) . o c= () . o by ; :: thesis: verum
end;
suppose A38: o = indx K ; :: thesis: (L +* ((indx K),(f . k))) . b1 c= () . b1
then (L +* ((indx K),(f . k))) . o = f . k by ;
then (L +* ((indx K),(f . k))) . o in rng f by ;
then (L +* ((indx K),(f . k))) . o c= the carrier of (A . (indx K)) ;
hence (L +* ((indx K),(f . k))) . o c= () . o by ; :: thesis: verum
end;
end;
end;
dom (L +* ((indx K),(f . k))) = I by PARTFUN1:def 2;
then product (L +* ((indx K),(f . k))) c= product () by ;
then aa c= product () by ;
hence a in bool the carrier of () ; :: thesis: verum
end;
A39: dom g = Seg (len f) by ;
reconsider g = g as FinSequence of bool the carrier of () by ;
len f in dom g by ;
then A40: g . (len f) in rng g by FUNCT_1:3;
then reconsider Yb = g . (len f) as Subset of () ;
A41: now :: thesis: for o being object st o in I holds
(L +* ((indx K),(f . 1))) . o = K . o
let o be object ; :: thesis: ( o in I implies (L +* ((indx K),(f . 1))) . b1 = K . b1 )
assume o in I ; :: thesis: (L +* ((indx K),(f . 1))) . b1 = K . b1
per cases ( o <> indx K or o = indx K ) ;
suppose A42: o <> indx K ; :: thesis: (L +* ((indx K),(f . 1))) . b1 = K . b1
then (L +* ((indx K),(f . 1))) . o = L . o by FUNCT_7:32;
hence (L +* ((indx K),(f . 1))) . o = K . o by ; :: thesis: verum
end;
suppose o = indx K ; :: thesis: (L +* ((indx K),(f . 1))) . b1 = K . b1
hence (L +* ((indx K),(f . 1))) . o = K . o by ; :: thesis: verum
end;
end;
end;
A43: for V being Subset of () st V in rng g holds
( V is closed_under_lines & V is strong )
proof
let V be Subset of (); :: 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 ;
then A46: n in dom f by FINSEQ_1:def 3;
not f . n is trivial
proof
A47: n <= len f by ;
per cases ( ( 1 <= n & n = len f ) or ( 1 <= n & n < len f ) ) by ;
suppose ( 1 <= n & n = len f ) ; :: thesis: not f . n is trivial
hence not f . n is trivial by A22; :: thesis: verum
end;
suppose A48: ( 1 <= n & n < len f ) ; :: thesis: not f . n is trivial
A49: card ((f . n) /\ (f . (n + 1))) c= card (f . n) by ;
2 c= card ((f . n) /\ (f . (n + 1))) by ;
then 2 c= card (f . n) by A49;
hence not f . n is trivial by PENCIL_1:4; :: thesis: verum
end;
end;
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: ( not o in I or (L +* ((indx K),(f . n))) . o c= () . o )
assume A51: o in I ; :: thesis: (L +* ((indx K),(f . n))) . o c= () . o
per cases ( o <> indx K or o = indx K ) ;
suppose A52: o <> indx K ; :: thesis: (L +* ((indx K),(f . n))) . o c= () . o
A53: L c= Carrier A by PBOOLE:def 18;
(L +* ((indx K),(f . n))) . o = L . o by ;
hence (L +* ((indx K),(f . n))) . o c= () . o by ; :: thesis: verum
end;
suppose A54: o = indx K ; :: thesis: (L +* ((indx K),(f . n))) . o c= () . o
then (L +* ((indx K),(f . n))) . o = f . n by ;
then (L +* ((indx K),(f . n))) . o in rng f by ;
then (L +* ((indx K),(f . n))) . o c= the carrier of (A . (indx K)) ;
hence (L +* ((indx K),(f . n))) . o c= () . o by ; :: thesis: verum
end;
end;
end;
L . (indx K) = [#] (A . (indx K)) by ;
then indx K = indx L by ;
then reconsider LI = L +* ((indx K),fn) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by ;
reconsider LI = LI as non trivial-yielding Segre-like ManySortedSubset of Carrier A ;
A55: LI . (indx K) = fn by ;
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 )
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 ;
hence ( D is strong & D is closed_under_lines ) by ; :: thesis: verum
end;
g . n = product (L +* ((indx K),(f . n))) by ;
hence ( V is closed_under_lines & V is strong ) by ; :: thesis: verum
end;
A58: len f in Seg (len f) by ;
then Yb = product EL by ;
then A59: ( not Yb is trivial & Yb is strong & Yb is closed_under_lines ) by ;
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 ;
then A64: g . i = product (L +* ((indx K),(f . i))) by ;
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 ;
reconsider l = l as ManySortedSet of I by ;
set l1 = l +* ((indx K),a);
set l2 = l +* ((indx K),b);
A70: i + 1 <= len g by ;
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
let o be object ; :: thesis: ( o in dom (L +* ((indx K),(f . i))) implies (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . i))) . b1 )
assume o in dom (L +* ((indx K),(f . i))) ; :: thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . i))) . b1
then A72: o in I ;
then A73: o in dom l by PARTFUN1:def 2;
per cases ( o = indx K or o <> indx K ) ;
suppose A74: o = indx K ; :: thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . i))) . b1
then (l +* ((indx K),a)) . o = a by ;
then (l +* ((indx K),a)) . o in f . i by ;
hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . i))) . o by ; :: thesis: verum
end;
suppose A75: o <> indx K ; :: thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . i))) . b1
then A76: (l +* ((indx K),a)) . o = l . o by FUNCT_7:32;
l . o in L . o by ;
hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . i))) . o by ; :: thesis: verum
end;
end;
end;
1 <= i + 1 by ;
then i + 1 in Seg (len f) by ;
then A77: g . (i + 1) = product (L +* ((indx K),(f . (i + 1)))) by ;
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
let o be object ; :: thesis: ( o in dom (L +* ((indx K),(f . i))) implies (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . i))) . b1 )
assume o in dom (L +* ((indx K),(f . i))) ; :: thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . i))) . b1
then A79: o in I ;
then A80: o in dom l by PARTFUN1:def 2;
per cases ( o = indx K or o <> indx K ) ;
suppose A81: o = indx K ; :: thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . i))) . b1
then (l +* ((indx K),b)) . o = b by ;
then (l +* ((indx K),b)) . o in f . i by ;
hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . i))) . o by ; :: thesis: verum
end;
suppose A82: o <> indx K ; :: thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . i))) . b1
then A83: (l +* ((indx K),b)) . o = l . o by FUNCT_7:32;
l . o in L . o by ;
hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . i))) . o by ; :: thesis: verum
end;
end;
end;
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
let o be object ; :: thesis: ( o in dom (L +* ((indx K),(f . (i + 1)))) implies (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1 )
assume o in dom (L +* ((indx K),(f . (i + 1)))) ; :: thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1
then A85: o in I ;
then A86: o in dom l by PARTFUN1:def 2;
per cases ( o = indx K or o <> indx K ) ;
suppose A87: o = indx K ; :: thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1
then (l +* ((indx K),a)) . o = a by ;
then (l +* ((indx K),a)) . o in f . (i + 1) by ;
hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . (i + 1)))) . o by ; :: thesis: verum
end;
suppose A88: o <> indx K ; :: thesis: (l +* ((indx K),a)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1
then A89: (l +* ((indx K),a)) . o = l . o by FUNCT_7:32;
l . o in L . o by ;
hence (l +* ((indx K),a)) . o in (L +* ((indx K),(f . (i + 1)))) . o by ; :: thesis: verum
end;
end;
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 ;
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
let o be object ; :: thesis: ( o in dom (L +* ((indx K),(f . (i + 1)))) implies (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1 )
assume o in dom (L +* ((indx K),(f . (i + 1)))) ; :: thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1
then A92: o in I ;
then A93: o in dom l by PARTFUN1:def 2;
per cases ( o = indx K or o <> indx K ) ;
suppose A94: o = indx K ; :: thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1
then (l +* ((indx K),b)) . o = b by ;
then (l +* ((indx K),b)) . o in f . (i + 1) by ;
hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . (i + 1)))) . o by ; :: thesis: verum
end;
suppose A95: o <> indx K ; :: thesis: (l +* ((indx K),b)) . b1 in (L +* ((indx K),(f . (i + 1)))) . b1
then A96: (l +* ((indx K),b)) . o = l . o by FUNCT_7:32;
l . o in L . o by ;
hence (l +* ((indx K),b)) . o in (L +* ((indx K),(f . (i + 1)))) . o by ; :: thesis: verum
end;
end;
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 ;
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 ;
then A98: l +* ((indx K),b) in (g . i) /\ (g . (i + 1)) by ;
(l +* ((indx K),a)) . (indx K) = a by ;
then A99: l +* ((indx K),a) <> l +* ((indx K),b) by ;
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 ;
then l +* ((indx K),a) in (g . i) /\ (g . (i + 1)) by ;
hence 2 c= card ((g . i) /\ (g . (i + 1))) by ; :: thesis: verum
end;
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
let o be object ; :: thesis: ( o in dom (L +* ((indx K),(f . (len f)))) implies z . b1 in (L +* ((indx K),(f . (len f)))) . b1 )
assume o in dom (L +* ((indx K),(f . (len f)))) ; :: thesis: z . b1 in (L +* ((indx K),(f . (len f)))) . b1
then A101: o in I ;
per cases ( o = indx K or o <> indx K ) ;
suppose o = indx K ; :: thesis: z . b1 in (L +* ((indx K),(f . (len f)))) . b1
hence z . o in (L +* ((indx K),(f . (len f)))) . o by ; :: thesis: verum
end;
suppose A102: o <> indx K ; :: thesis: z . b1 in (L +* ((indx K),(f . (len f)))) . b1
z . o in L . o by ;
hence z . o in (L +* ((indx K),(f . (len f)))) . o by ; :: thesis: verum
end;
end;
end;
L +* ((indx K),(f . 1)) = K by A41;
then W = g . 1 by A3, A27, A39, A21;
then W,Yb are_joinable by ;
then A103: Yb in { Y where Y is Subset of () : ( 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 ;
then y in Yb by ;
hence y in C by ; :: thesis: verum
end;
dom K = I by PARTFUN1:def 2;
then A104: L . (indx L) = [#] (A . (indx L)) by ;
C c= product L
proof
let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in C or c in product L )
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 () : ( 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 () 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 ;
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 ;
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: ( 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 ;
per cases ( a = indx K or a <> indx K ) ;
suppose A115: a = indx K ; :: thesis: c1 . a in L . a
M c= Carrier A by PBOOLE:def 18;
then M . a1 c= () . a1 ;
then A116: M . a1 c= the carrier of (A . a1) by YELLOW_6:2;
c1 . a in M . a by ;
then c1 . a in [#] (A . (indx K)) by ;
hence c1 . a in L . a by ; :: thesis: verum
end;
suppose A117: a <> indx K ; :: thesis: c1 . a in L . a
c1 . a in M . a by ;
then c1 . a in K . a by A2, A3, A108, A109, A110, A117, Th11;
hence c1 . a in L . a by ; :: thesis: verum
end;
end;
end;
dom c1 = I by PARTFUN1:def 2
.= dom L by PARTFUN1:def 2 ;
hence c in product L by ; :: thesis: verum
end;
then C = product L by A9;
hence union { Y where Y is Subset of () : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A by ; :: thesis: verum