let I be non empty set ; 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; ( ( 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
; 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); ( 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 )
; 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)
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 ;
TARSKI:def 3 ( 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
;
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
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 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 FINSEQ_1:sch 2();
A28:
rng g c= bool the
carrier of
(Segre_Product A)
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) ;
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);
( V in rng g implies ( V is closed_under_lines & V is strong ) )
assume
V in rng g
;
( 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
then reconsider fn =
f . n as non
trivial set ;
A50:
L +* (
(indx K),
(f . n))
c= Carrier A
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;
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;
verum
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 ;
( 1 <= i & i < len g implies 2 c= card ((g . i) /\ (g . (i + 1))) )
assume that A62:
1
<= i
and A63:
i < len g
;
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;
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;
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;
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;
verum
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;
verum
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 ;
TARSKI:def 3 ( not c in C or c in product L )
assume
c in C
;
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
let a be
object ;
( a in dom L implies c1 . a in L . a )
assume A114:
a in dom L
;
c1 . a in L . a
then reconsider a1 =
a as
Element of
I ;
per cases
( a = indx K or a <> indx K )
;
suppose A117:
a <> indx K
;
c1 . a in L . a
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;
verum end;
end;
dom c1 =
I
by PARTFUN1:def 2
.=
dom L
by PARTFUN1:def 2
;
hence
c in product L
by A113, CARD_3:9;
verum
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; verum