let f be ManySortedSet of I; :: thesis: ( f is Segre-like & not f is trivial-yielding implies f is non-empty )
assume ( f is Segre-like & not f is trivial-yielding ) ; :: thesis: f is non-empty
then reconsider g = f as non trivial-yielding Segre-like ManySortedSet of I ;

now :: thesis: not {} in rng g

assume {} in rng g ; :: thesis: contradiction
then consider i being object such that
A1: i in dom f and
A2: g . i = {} by FUNCT_1:def 3;
reconsider i = i as Element of I by A1, PARTFUN1:def 2;

per cases ( i = indx g or i <> indx g ) ;

suppose i = indx g ; :: thesis: contradiction

hence contradiction by A2, Def21; :: thesis: verum

end;

suppose i <> indx g ; :: thesis: contradiction

then g . i is 1 -element by Th12;
hence contradiction by A2; :: thesis: verum

end;

end;

end;

hence f is non-empty by RELAT_1:def 9; :: thesis: verum