consider i being Element of I;
consider B being ManySortedSet of ;
take C = {B} +* i,{0 ,1}; :: thesis: ( C is Segre-like & not C is trivial-yielding )
thus C is Segre-like :: thesis: not C is trivial-yielding

proof

take i ; :: according to PENCIL_1:def 20 :: thesis: for j being Element of I st i <> j holds
( not C . j is empty & C . j is trivial )
let j be Element of I; :: thesis: ( i <> j implies ( not C . j is empty & C . j is trivial ) )
j in I ;
then A1: j in dom {B} by PARTFUN1:def 4;
assume j <> i ; :: thesis: ( not C . j is empty & C . j is trivial )
then A2: C . j = {B} . j by FUNCT_7:34;
then C . j in rng {B} by A1, FUNCT_1:def 5;
hence ( not C . j is empty & C . j is trivial ) by A1, A2, Def16, FUNCT_1:def 15; :: thesis: verum

end;

thus not C is trivial-yielding :: thesis: verum

proof

take S = C . i; :: according to PENCIL_1:def 16 :: thesis: ( S in rng C & not S is trivial )
dom C = I by PARTFUN1:def 4;
hence S in rng C by FUNCT_1:def 5; :: thesis: not S is trivial
dom {B} = I by PARTFUN1:def 4;
then A3: C . i = {0 ,1} by FUNCT_7:33;
( 0 in {0 ,1} & 1 in {0 ,1} ) by TARSKI:def 2;
then 2 c= card {0 ,1} by Th2;
hence not S is trivial by A3, Th4; :: thesis: verum

end;