let I be non empty set ; for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds
( A . i is identifying_close_blocks & A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) holds
Segre_Product A is identifying_close_blocks
let A be non-Empty TopStruct-yielding ManySortedSet of I; ( ( for i being Element of I holds
( A . i is identifying_close_blocks & A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) implies Segre_Product A is identifying_close_blocks )
assume A1:
for i being Element of I holds
( A . i is identifying_close_blocks & A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void )
; Segre_Product A is identifying_close_blocks
for k, l being Block of (Segre_Product A) st 2 c= card (k /\ l) holds
k = l
proof
let k,
l be
Block of
(Segre_Product A);
( 2 c= card (k /\ l) implies k = l )
assume
2
c= card (k /\ l)
;
k = l
then consider a,
b being
object such that A2:
a in k /\ l
and A3:
b in k /\ l
and A4:
a <> b
by Th2;
not
Segre_Product A is
void
by A1, Th15;
then consider B being
Segre-like ManySortedSubset of
Carrier A such that A5:
k = product B
and A6:
ex
i being
Element of
I st
B . i is
Block of
(A . i)
by Def22;
A7:
b in product B
by A5, A3, XBOOLE_0:def 4;
then reconsider b =
b as
Function by CARD_3:48;
A8:
dom b =
dom B
by A7, CARD_3:9
.=
I
by PARTFUN1:def 2
;
then reconsider b =
b as
ManySortedSet of
I by PARTFUN1:def 2, RELAT_1:def 18;
A9:
a in product B
by A5, A2, XBOOLE_0:def 4;
consider i being
Element of
I such that A10:
B . i is
Block of
(A . i)
by A6;
A11:
for
j being
Element of
I st
j <> i holds
B . j is 1
-element
not
Segre_Product A is
void
by A1, Th15;
then consider C being
Segre-like ManySortedSubset of
Carrier A such that A14:
l = product C
and A15:
ex
i being
Element of
I st
C . i is
Block of
(A . i)
by Def22;
A16:
dom C = I
by PARTFUN1:def 2;
consider j being
Element of
I such that A17:
C . j is
Block of
(A . j)
by A15;
reconsider a =
a as
Function by A9, CARD_3:48;
A18:
dom a =
dom B
by A9, CARD_3:9
.=
I
by PARTFUN1:def 2
;
then reconsider a =
a as
ManySortedSet of
I by PARTFUN1:def 2, RELAT_1:def 18;
consider x being
object such that A19:
x in I
and A20:
a . x <> b . x
by A4, A18, A8, FUNCT_1:2;
reconsider x =
x as
Element of
I by A19;
dom B = I
by PARTFUN1:def 2;
then A21:
b . x in B . x
by A7, CARD_3:9;
dom B = I
by PARTFUN1:def 2;
then A22:
a . x in B . x
by A9, CARD_3:9;
then
2
c= card (B . x)
by A20, A21, Th2;
then
not
B . x is 1
-element
by Th4;
then A23:
x = i
by A11;
b in product C
by A14, A3, XBOOLE_0:def 4;
then A24:
b . x in C . x
by A16, CARD_3:9;
A25:
a in product C
by A14, A2, XBOOLE_0:def 4;
A26:
for
i being
Element of
I st
j <> i holds
C . i is 1
-element
A29:
dom B =
I
by PARTFUN1:def 2
.=
dom C
by PARTFUN1:def 2
;
dom C = I
by PARTFUN1:def 2;
then A30:
a . x in C . x
by A25, CARD_3:9;
then
2
c= card (C . x)
by A20, A24, Th2;
then
not
C . x is 1
-element
by Th4;
then A31:
x = j
by A26;
for
s being
object st
s in dom B holds
B . s c= C . s
proof
let s be
object ;
( s in dom B implies B . s c= C . s )
assume A32:
s in dom B
;
B . s c= C . s
then reconsider t =
s as
Element of
I by PARTFUN1:def 2;
per cases
( t = x or s <> x )
;
suppose A33:
t = x
;
B . s c= C . sthen reconsider Ct =
C . t as
Block of
(A . t) by A17, A31;
reconsider Bt =
B . t as
Block of
(A . t) by A10, A23, A33;
(
a . t in Bt /\ Ct &
b . t in Bt /\ Ct )
by A22, A21, A30, A24, A33, XBOOLE_0:def 4;
then A34:
2
c= card (Bt /\ Ct)
by A20, A33, Th2;
A . t is
identifying_close_blocks
by A1;
hence
B . s c= C . s
by A34;
verum end;
end;
hence
k c= l
by A5, A14, A29, CARD_3:27;
XBOOLE_0:def 10 l c= k
for
s being
object st
s in dom C holds
C . s c= B . s
proof
let s be
object ;
( s in dom C implies C . s c= B . s )
assume A37:
s in dom C
;
C . s c= B . s
then reconsider t =
s as
Element of
I by PARTFUN1:def 2;
per cases
( t = x or s <> x )
;
suppose A38:
t = x
;
C . s c= B . sthen reconsider Ct =
C . t as
Block of
(A . t) by A17, A31;
reconsider Bt =
B . t as
Block of
(A . t) by A10, A23, A38;
(
a . t in Bt /\ Ct &
b . t in Bt /\ Ct )
by A22, A21, A30, A24, A38, XBOOLE_0:def 4;
then A39:
2
c= card (Bt /\ Ct)
by A20, A38, Th2;
A . t is
identifying_close_blocks
by A1;
hence
C . s c= B . s
by A39;
verum end;
end;
hence
l c= k
by A5, A14, A29, CARD_3:27;
verum
end;
hence
Segre_Product A is identifying_close_blocks
; verum