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
(A +* ((indx A),N)) . j is 1 -element
let i be Element of I; :: thesis: ( indx A <> i implies (A +* ((indx A),N)) . i is 1 -element )
assume A1: i <> indx A ; :: thesis: (A +* ((indx A),N)) . i is 1 -element
then (A +* ((indx A),N)) . i = A . i by FUNCT_7:32;
hence (A +* ((indx A),N)) . i is 1 -element 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 2;
hence (A +* ((indx A),N)) . (indx A) in rng (A +* ((indx A),N)) by FUNCT_1:def 3; :: thesis: not (A +* ((indx A),N)) . (indx A) is trivial
I = dom A by PARTFUN1:def 2;
hence not (A +* ((indx A),N)) . (indx A) is trivial by FUNCT_7:31; :: thesis: verum

end;