let I be non empty set ; :: thesis: for A being non-Empty TopStruct-yielding ManySortedSet of 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 ; :: thesis: ( ( 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 ) ; :: thesis: 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); :: thesis: ( 2 c= card (k /\ l) implies k = l )
not Segre_Product A is void by A1, Th15;
then not Segre_Blocks A is empty ;
then consider B being Segre-like ManySortedSubset of Carrier A such that
A2: ( k = product B & ex i being Element of I st B . i is Block of (A . i) ) by Def22;
consider i being Element of I such that
A3: B . i is Block of (A . i) by A2;
A4: for j being Element of I st j <> i holds
( not B . j is empty & B . j is trivial )

proof

let j be Element of I; :: thesis: ( j <> i implies ( not B . j is empty & B . j is trivial ) )
assume A5: j <> i ; :: thesis: ( not B . j is empty & B . j is trivial )
consider i1 being Element of I such that
A6: for j1 being Element of I st j1 <> i1 holds
( not B . j1 is empty & B . j1 is trivial ) by Def20;
A . i is with_non_trivial_blocks by A1;
then 2 c= card (B . i) by A3, Def6;
then not B . i is trivial by Th4;
then i1 = i by A6;
hence ( not B . j is empty & B . j is trivial ) by A5, A6; :: thesis: verum

end;

not Segre_Product A is void by A1, Th15;
then not Segre_Blocks A is empty ;
then consider C being Segre-like ManySortedSubset of Carrier A such that
A7: ( l = product C & ex i being Element of I st C . i is Block of (A . i) ) by Def22;
consider j being Element of I such that
A8: C . j is Block of (A . j) by A7;
A9: for i being Element of I st j <> i holds
( not C . i is empty & C . i is trivial )

proof

let i be Element of I; :: thesis: ( j <> i implies ( not C . i is empty & C . i is trivial ) )
assume A10: j <> i ; :: thesis: ( not C . i is empty & C . i is trivial )
consider j1 being Element of I such that
A11: for i1 being Element of I st j1 <> i1 holds
( not C . i1 is empty & C . i1 is trivial ) by Def20;
A . j is with_non_trivial_blocks by A1;
then 2 c= card (C . j) by A8, Def6;
then not C . j is trivial by Th4;
then j1 = j by A11;
hence ( not C . i is empty & C . i is trivial ) by A10, A11; :: thesis: verum

end;

assume 2 c= card (k /\ l) ; :: thesis: k = l
then consider a, b being set such that
A12: ( a in k /\ l & b in k /\ l & a <> b ) by Th2;
A13: a in product B by A2, A12, XBOOLE_0:def 4;
then reconsider a = a as Function by CARD_3:64;
A14: b in product B by A2, A12, XBOOLE_0:def 4;
then reconsider b = b as Function by CARD_3:64;
A15: dom a = dom B by A13, CARD_3:18
.= I by PARTFUN1:def 4 ;
then reconsider a = a as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
A16: dom b = dom B by A14, CARD_3:18
.= I by PARTFUN1:def 4 ;
then reconsider b = b as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
consider x being set such that
A17: ( x in I & a . x <> b . x ) by A12, A15, A16, FUNCT_1:9;
reconsider x = x as Element of I by A17;
dom B = I by PARTFUN1:def 4;
then A18: a . x in B . x by A13, CARD_3:18;
dom B = I by PARTFUN1:def 4;
then A19: b . x in B . x by A14, CARD_3:18;
then 2 c= card (B . x) by A17, A18, Th2;
then not B . x is trivial by Th4;
then A20: x = i by A4;
A21: a in product C by A7, A12, XBOOLE_0:def 4;
dom C = I by PARTFUN1:def 4;
then A22: a . x in C . x by A21, CARD_3:18;
A23: b in product C by A7, A12, XBOOLE_0:def 4;
dom C = I by PARTFUN1:def 4;
then A24: b . x in C . x by A23, CARD_3:18;
then 2 c= card (C . x) by A17, A22, Th2;
then not C . x is trivial by Th4;
then A25: x = j by A9;
A26: dom B = I by PARTFUN1:def 4
.= dom C by PARTFUN1:def 4 ;
for s being set st s in dom B holds
B . s c= C . s

proof

let s be set ; :: thesis: ( s in dom B implies B . s c= C . s )
assume A27: s in dom B ; :: thesis: B . s c= C . s
then reconsider t = s as Element of I by PARTFUN1:def 4;

per cases ( t = x or s <> x ) ;

suppose A28: t = x ; :: thesis: B . s c= C . s

then reconsider Bt = B . t as Block of (A . t) by A3, A20;
reconsider Ct = C . t as Block of (A . t) by A8, A25, A28;
A29: a . t in Bt /\ Ct by A18, A22, A28, XBOOLE_0:def 4;
b . t in Bt /\ Ct by A19, A24, A28, XBOOLE_0:def 4;
then A30: 2 c= card (Bt /\ Ct) by A17, A28, A29, Th2;
A . t is identifying_close_blocks by A1;
hence B . s c= C . s by A30, Def7; :: thesis: verum

end;

suppose s <> x ; :: thesis: B . s c= C . s

then ( not B . t is empty & B . t is trivial ) by A4, A20;
then consider y being set such that
A31: B . t = {y} by REALSET1:def 4;
a . t in B . t by A13, A27, CARD_3:18;
then A32: a . t = y by A31, TARSKI:def 1;
a . t in C . t by A21, A26, A27, CARD_3:18;
hence B . s c= C . s by A31, A32, ZFMISC_1:37; :: thesis: verum

end;

end;

end;

hence k c= l by A2, A7, A26, CARD_3:38; :: according to XBOOLE_0:def 10 :: thesis: l c= k
for s being set st s in dom C holds
C . s c= B . s

proof

let s be set ; :: thesis: ( s in dom C implies C . s c= B . s )
assume A33: s in dom C ; :: thesis: C . s c= B . s
then reconsider t = s as Element of I by PARTFUN1:def 4;

per cases ( t = x or s <> x ) ;

suppose A34: t = x ; :: thesis: C . s c= B . s

then reconsider Bt = B . t as Block of (A . t) by A3, A20;
reconsider Ct = C . t as Block of (A . t) by A8, A25, A34;
A35: a . t in Bt /\ Ct by A18, A22, A34, XBOOLE_0:def 4;
b . t in Bt /\ Ct by A19, A24, A34, XBOOLE_0:def 4;
then A36: 2 c= card (Bt /\ Ct) by A17, A34, A35, Th2;
A . t is identifying_close_blocks by A1;
hence C . s c= B . s by A36, Def7; :: thesis: verum

end;

suppose s <> x ; :: thesis: C . s c= B . s

then ( not C . t is empty & C . t is trivial ) by A9, A25;
then consider y being set such that
A37: C . t = {y} by REALSET1:def 4;
a . t in C . t by A21, A33, CARD_3:18;
then A38: a . t = y by A37, TARSKI:def 1;
a . t in B . t by A13, A26, A33, CARD_3:18;
hence C . s c= B . s by A37, A38, ZFMISC_1:37; :: thesis: verum

end;

end;

end;

hence l c= k by A2, A7, A26, CARD_3:38; :: thesis: verum

end;

hence Segre_Product A is identifying_close_blocks by Def7; :: thesis: verum