set B = the ManySortedSet of I;
set i = the Element of I;
take C = { the ManySortedSet of I} +* ( the Element of 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 the Element of I ; :: according to PENCIL_1:def 20 :: thesis: for j being Element of I st the Element of I <> j holds
C . j is 1 -element
let j be Element of I; :: thesis: ( the Element of I <> j implies C . j is 1 -element )
assume j <> the Element of I ; :: thesis: C . j is 1 -element
then A1: C . j = { the ManySortedSet of I} . j by FUNCT_7:32;
j in I ;
then A2: j in dom { the ManySortedSet of I} by PARTFUN1:def 2;
then C . j in rng { the ManySortedSet of I} by A1, FUNCT_1:def 3;
then ( not C . j is empty & C . j is trivial ) by A2, A1, Def16, FUNCT_1:def 9;
hence C . j is 1 -element ; :: thesis: verum
end;
thus not C is trivial-yielding :: thesis: verum
proof
take S = C . the Element of I; :: according to PENCIL_1:def 16 :: thesis: ( S in rng C & not S is trivial )
dom C = I by PARTFUN1:def 2;
hence S in rng C by FUNCT_1:def 3; :: thesis: not S is trivial
dom { the ManySortedSet of I} = I by PARTFUN1:def 2;
then A3: C . the Element of I = {0,1} by FUNCT_7:31;
( 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;