let I be non empty set ; :: thesis:
let A be non-Empty TopStruct-yielding ManySortedSet of ; :: thesis:
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:
A2: not the topology of (A . i) is empty by A1;
consider l being Block of (A . i);
A3: for j being Element of I st i <> j holds
( not (B +* i,l) . j is empty & (B +* i,l) . j is trivial )

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

end;

B +* i,l c= Carrier A

let i1 be set ; :: according to PBOOLE:def 5 :: thesis:
assume A6: i1 in I ; :: thesis:
then A7: i1 in dom B by PARTFUN1:def 4;

per cases ;

suppose A8: i = i1 ; :: thesis:

then (B +* i,l) . i1 = l by A7, FUNCT_7:33;
then A9: (B +* i,l) . i1 in the topology of (A . i) by A2;
consider R being 1-sorted such that
A10: ( R = A . i1 & the carrier of R = (Carrier A) . i1 ) by A6, PRALG_1:def 13;
thus (B +* i,l) . i1 c= (Carrier A) . i1 by A8, A9, A10; :: thesis:

end;

suppose i1 <> i ; :: thesis:

then A11: (B +* i,l) . i1 = B . i1 by FUNCT_7:34;
B c= Carrier A by PBOOLE:def 23;
hence (B +* i,l) . i1 c= (Carrier A) . i1 by A6, A11, PBOOLE:def 5; :: thesis:

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: