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 )
consider B being 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
consider l being Block of (A . i);
A2: not the topology of (A . i) is empty by A1;
A3: B +* (i,l) c= Carrier A

proof

let i1 be set ; :: according to PBOOLE:def 5 :: thesis: ( not i1 in I or (B +* (i,l)) . i1 c= (Carrier A) . i1 )
assume A4: i1 in I ; :: thesis: (B +* (i,l)) . i1 c= (Carrier A) . i1
then A5: i1 in dom B by PARTFUN1:def 4;

per cases ( i = i1 or i1 <> i ) ;

suppose A6: i = i1 ; :: thesis: (B +* (i,l)) . i1 c= (Carrier A) . i1

then (B +* (i,l)) . i1 = l by A5, FUNCT_7:33;
then A7: (B +* (i,l)) . 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 (B +* (i,l)) . i1 c= (Carrier A) . i1 by A6, A7; :: thesis: verum

end;

suppose A8: i1 <> i ; :: thesis: (B +* (i,l)) . i1 c= (Carrier A) . i1

A9: B c= Carrier A by PBOOLE:def 23;
(B +* (i,l)) . i1 = B . i1 by A8, FUNCT_7:34;
hence (B +* (i,l)) . i1 c= (Carrier A) . i1 by A4, A9, PBOOLE:def 5; :: thesis: verum

end;

end;

end;

for j being Element of I st i <> j holds
( not (B +* (i,l)) . j is empty & (B +* (i,l)) . j is trivial )

proof

let j be Element of I; :: thesis: ( i <> j implies ( not (B +* (i,l)) . j is empty & (B +* (i,l)) . j is trivial ) )
assume i <> j ; :: thesis: ( not (B +* (i,l)) . j is empty & (B +* (i,l)) . j is trivial )
then A10: (B +* (i,l)) . j = B . j by FUNCT_7:34;
j in I ;
then A11: j in dom B by PARTFUN1:def 4;
then (B +* (i,l)) . j in rng B by A10, FUNCT_1:def 5;
hence ( not (B +* (i,l)) . j is empty & (B +* (i,l)) . j is trivial ) by A11, A10, Def16, FUNCT_1:def 15; :: thesis: verum

end;

then reconsider C = B +* (i,l) as Segre-like ManySortedSubset of Carrier A by A3, Def20, PBOOLE:def 23;
dom B = 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