consider B being Element of Carrier A;
consider i1 being Element of I;
A1: ex R being 1-sorted st
( R = A . i1 & the carrier of R = (Carrier A) . i1 ) by PRALG_1:def 13;
then reconsider b1 = B . i1 as Element of (A . i1) by PBOOLE:def 17;
reconsider B = B as ManySortedSet of I ;
dom A = I by PARTFUN1:def 4;
then A . i1 in rng A by FUNCT_1:def 5;
then not A . i1 is trivial by Def17;
then reconsider Ai1 = the carrier of (A . i1) as non trivial set ;
ex x1, x2 being Element of Ai1 st x1 <> x2 by YELLOW_8:def 1;
then 2 c= card the carrier of (A . i1) by Th2;
then consider b2 being set such that
A2: b2 in the carrier of (A . i1) and
A3: b1 <> b2 by Th3;
reconsider b2 = b2 as Element of (A . i1) by A2;
set B1 = B +* i1,b2;
A4: for i being set st i in I holds
(B +* i1,b2) . i is Element of (Carrier A) . i

proof

let i be set ; :: thesis: ( i in I implies (B +* i1,b2) . i is Element of (Carrier A) . i )
assume A5: i in I ; :: thesis: (B +* i1,b2) . i is Element of (Carrier A) . i

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

suppose i <> i1 ; :: thesis: (B +* i1,b2) . i is Element of (Carrier A) . i

then (B +* i1,b2) . i = B . i by FUNCT_7:34;
hence (B +* i1,b2) . i is Element of (Carrier A) . i by A5, PBOOLE:def 17; :: thesis: verum

end;

suppose A6: i = i1 ; :: thesis: (B +* i1,b2) . i is Element of (Carrier A) . i

then i1 in dom B by A5, PARTFUN1:def 4;
hence (B +* i1,b2) . i is Element of (Carrier A) . i by A1, A6, FUNCT_7:33; :: thesis: verum

end;

end;

end;

{B,(B +* i1,b2)} c= Carrier A

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or {B,(B +* i1,b2)} . i c= (Carrier A) . i )
assume A7: i in I ; :: thesis: {B,(B +* i1,b2)} . i c= (Carrier A) . i
then reconsider j = i as Element of I ;
j in dom A by A7, PARTFUN1:def 4;
then A . j in rng A by FUNCT_1:def 5;
then A8: not A . j is empty by YELLOW_6:def 4;
B . j is Element of (Carrier A) . j by PBOOLE:def 17;
then A9: B . j is Element of (A . j) by YELLOW_6:9;
(B +* i1,b2) . j is Element of (Carrier A) . j by A4;
then (B +* i1,b2) . j is Element of (A . j) by YELLOW_6:9;
then {(B . j),((B +* i1,b2) . j)} c= the carrier of (A . j) by A8, A9, ZFMISC_1:38;
then {B,(B +* i1,b2)} . j c= the carrier of (A . j) by PZFMISC1:def 2;
hence {B,(B +* i1,b2)} . i c= (Carrier A) . i by YELLOW_6:9; :: thesis: verum

end;

then reconsider C = {B,(B +* i1,b2)} as ManySortedSubset of Carrier A by PBOOLE:def 23;
dom B = I by PARTFUN1:def 4;
then (B +* i1,b2) . i1 = b2 by FUNCT_7:33;
then A10: C . i1 = {b1,b2} by PZFMISC1:def 2;

A11: now

assume C . i1 is trivial ; :: thesis: contradiction
then ( C . i1 is empty or ex x being set st C . i1 = {x} ) by REALSET1:def 4;
hence contradiction by A3, A10, ZFMISC_1:9; :: thesis: verum

end;

take C ; :: thesis: ( C is Segre-like & not C is trivial-yielding & C is non-empty )
thus C is Segre-like :: thesis: ( not C is trivial-yielding & C is non-empty )

proof

take i1 ; :: according to PENCIL_1:def 20 :: thesis: for j being Element of I st i1 <> j holds
( not C . j is empty & C . j is trivial )
let j be Element of I; :: thesis: ( i1 <> j implies ( not C . j is empty & C . j is trivial ) )
assume i1 <> j ; :: thesis: ( not C . j is empty & C . j is trivial )
then B . j = (B +* i1,b2) . j by FUNCT_7:34;
then C . j = {(B . j),(B . j)} by PZFMISC1:def 2
.= {(B . j)} by ENUMSET1:69 ;
hence ( not C . j is empty & C . j is trivial ) ; :: thesis: verum

end;

dom C = I by PARTFUN1:def 4;
then C . i1 in rng C by FUNCT_1:def 5;
hence not C is trivial-yielding by A11, Def16; :: thesis: C is non-empty
thus C is non-empty ; :: thesis: verum