let I be non empty set ; :: thesis: for A being non trivial-yielding Segre-like ManySortedSet of
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 ; :: 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;