let I be non empty set ; :: thesis: for A being non trivial-yielding Segre-like ManySortedSet of I
for N being non trivial set holds
( A +* ((indx A),N) is Segre-like & not A +* ((indx A),N) is trivial-yielding )
let A be non trivial-yielding Segre-like ManySortedSet of I; :: thesis: for N being non trivial set holds
( A +* ((indx A),N) is Segre-like & not A +* ((indx A),N) is trivial-yielding )
let N be non trivial set ; :: thesis: ( A +* ((indx A),N) is Segre-like & not A +* ((indx A),N) is trivial-yielding )
thus A +* ((indx A),N) is Segre-like :: thesis: not A +* ((indx A),N) is trivial-yielding

proof

take indx A ; :: according to PENCIL_1:def 20 :: thesis: for j being Element of I st indx A <> j holds
( not (A +* ((indx A),N)) . j is empty & (A +* ((indx A),N)) . j is trivial )
let i be Element of I; :: thesis: ( indx A <> i implies ( not (A +* ((indx A),N)) . i is empty & (A +* ((indx A),N)) . i is trivial ) )
assume A1: i <> indx A ; :: thesis: ( not (A +* ((indx A),N)) . i is empty & (A +* ((indx A),N)) . i is trivial )
then (A +* ((indx A),N)) . i = A . i by FUNCT_7:34;
hence ( not (A +* ((indx A),N)) . i is empty & (A +* ((indx A),N)) . i is trivial ) by A1, Th12; :: thesis: verum

end;

thus not A +* ((indx A),N) is trivial-yielding :: thesis: verum

proof

take (A +* ((indx A),N)) . (indx A) ; :: according to PENCIL_1:def 16 :: thesis: ( (A +* ((indx A),N)) . (indx A) in rng (A +* ((indx A),N)) & not (A +* ((indx A),N)) . (indx A) is trivial )
dom (A +* ((indx A),N)) = I by PARTFUN1:def 4;
hence (A +* ((indx A),N)) . (indx A) in rng (A +* ((indx A),N)) by FUNCT_1:def 5; :: thesis: not (A +* ((indx A),N)) . (indx A) is trivial
I = dom A by PARTFUN1:def 4;
hence not (A +* ((indx A),N)) . (indx A) is trivial by FUNCT_7:33; :: thesis: verum

end;