let f be ManySortedSet of ; :: 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 ;

now

assume {} in rng g ; :: thesis: contradiction
then consider i being set such that
A1: ( i in dom f & g . i = {} ) by FUNCT_1:def 5;
reconsider i = i as Element of I by A1, PARTFUN1:def 4;

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

suppose i = indx g ; :: thesis: contradiction

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

end;

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

hence contradiction by A1, Th12; :: thesis: verum

end;

end;

end;

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