let I be non empty set ; :: thesis: for A being non-Empty TopStruct-yielding ManySortedSet of I st not for i being Element of I holds A . i is void holds
not Segre_Product A is void
let A be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: ( not for i being Element of I holds A . i is void implies not Segre_Product A is void )
set B = the V5() trivial-yielding ManySortedSubset of Carrier A;
given i being Element of I such that A1: not A . i is void ; :: thesis: not Segre_Product A is void
set l = the Block of (A . i);
A2: not the topology of (A . i) is empty by A1;
A3: the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i)) c= Carrier A
proof
let i1 be set ; :: according to PBOOLE:def 5 :: thesis: ( not i1 in I or ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1 )
assume A4: i1 in I ; :: thesis: ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1
then A5: i1 in dom the V5() trivial-yielding ManySortedSubset of Carrier A by PARTFUN1:def 4;
per cases ( i = i1 or i1 <> i ) ;
suppose A6: i = i1 ; :: thesis: ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1
then ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 = the Block of (A . i) by A5, FUNCT_7:33;
then A7: ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 in the topology of (A . i) by A2;
ex R being 1-sorted st
( R = A . i1 & the carrier of R = (Carrier A) . i1 ) by A4, PRALG_1:def 13;
hence ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1 by A6, A7; :: thesis: verum
end;
end;
end;
for j being Element of I st i <> j holds
( not ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is empty & ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is trivial )
proof
let j be Element of I; :: thesis: ( i <> j implies ( not ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is empty & ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is trivial ) )
assume i <> j ; :: thesis: ( not ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is empty & ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is trivial )
then A10: ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j = the V5() trivial-yielding ManySortedSubset of Carrier A . j by FUNCT_7:34;
j in I ;
then A11: j in dom the V5() trivial-yielding ManySortedSubset of Carrier A by PARTFUN1:def 4;
then ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j in rng the V5() trivial-yielding ManySortedSubset of Carrier A by A10, FUNCT_1:def 5;
hence ( not ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is empty & ( the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is trivial ) by A11, A10, Def16, FUNCT_1:def 15; :: thesis: verum
end;
then reconsider C = the V5() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i)) as Segre-like ManySortedSubset of Carrier A by A3, Def20, PBOOLE:def 23;
dom the V5() trivial-yielding ManySortedSubset of Carrier A = I by PARTFUN1:def 4;
then C . i is Block of (A . i) by FUNCT_7:33;
then product C in Segre_Blocks A by Def22;
hence not Segre_Product A is void by Def4; :: thesis: verum