let k be Block of (Segre_Product A); :: thesis: 2 c= card k
not Segre_Product A is void by A1, Th15;
then consider B being Segre-like ManySortedSubset of Carrier A such that
A2: k = product B and
A3: ex i being Element of I st B . i is Block of (A . i) by Def22;
consider i being Element of I such that
A4: B . i is Block of (A . i) by A3;
A . i is with_non_trivial_blocks by A1;
then 2 c= card (B . i) by A4;
then A5: not B . i is trivial by Th4;
dom B = I by PARTFUN1:def 2;
then B . i in rng B by FUNCT_1:def 3;
then reconsider BB = B as non trivial-yielding Segre-like ManySortedSet of I by A5, Def16;
not product BB is trivial ;
hence 2 c= card k by A2, Th4; :: thesis: verum