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 non-empty 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 non-empty trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i)) c= Carrier A
proof
let i1 be object ; :: according to PBOOLE:def 2 :: thesis: ( not i1 in I or ( the non-empty trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1 )
assume A4: i1 in I ; :: thesis: ( the non-empty trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1
then A5: i1 in dom the non-empty trivial-yielding ManySortedSubset of Carrier A by PARTFUN1:def 2;
per cases ( i = i1 or i1 <> i ) ;
suppose A6: i = i1 ; :: thesis: ( the non-empty trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1
then ( the non-empty trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 = the Block of (A . i) by A5, FUNCT_7:31;
then A7: ( the non-empty 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 15;
hence ( the non-empty 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
( the non-empty trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is 1 -element
proof
let j be Element of I; :: thesis: ( i <> j implies ( the non-empty trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is 1 -element )
assume i <> j ; :: thesis: ( the non-empty trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is 1 -element
then A10: ( the non-empty trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j = the non-empty trivial-yielding ManySortedSubset of Carrier A . j by FUNCT_7:32;
j in I ;
then A11: j in dom the non-empty trivial-yielding ManySortedSubset of Carrier A by PARTFUN1:def 2;
then ( the non-empty trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j in rng the non-empty trivial-yielding ManySortedSubset of Carrier A by A10, FUNCT_1:def 3;
then ( not ( the non-empty trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is empty & ( the non-empty trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is trivial ) by A11, A10, Def16, FUNCT_1:def 9;
hence ( the non-empty trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is 1 -element ; :: thesis: verum
end;
then reconsider C = the non-empty trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i)) as Segre-like ManySortedSubset of Carrier A by A3, Def20, PBOOLE:def 18;
dom the non-empty trivial-yielding ManySortedSubset of Carrier A = I by PARTFUN1:def 2;
then C . i is Block of (A . i) by FUNCT_7:31;
then product C in Segre_Blocks A by Def22;
hence not Segre_Product A is void ; :: thesis: verum