let I be non empty set ; :: thesis: for A being non trivial-yielding Segre-like ManySortedSet of I
for x, y being ManySortedSet of I st x in product A & y in product A holds
for i being object st i <> indx A holds
x . i = y . i
let A be non trivial-yielding Segre-like ManySortedSet of I; :: thesis: for x, y being ManySortedSet of I st x in product A & y in product A holds
for i being object st i <> indx A holds
x . i = y . i
let x, y be ManySortedSet of I; :: thesis: ( x in product A & y in product A implies for i being object st i <> indx A holds
x . i = y . i )
assume that
A1: x in product A and
A2: y in product A ; :: thesis: for i being object st i <> indx A holds
x . i = y . i
let i be object ; :: thesis: ( i <> indx A implies x . i = y . i )
A3: dom A = I by PARTFUN1:def 2;
assume A4: i <> indx A ; :: thesis: x . i = y . i

per cases ( not i in I or i in I ) ;

suppose A5: not i in I ; :: thesis: x . i = y . i

then A6: not i in dom y by PARTFUN1:def 2;
not i in dom x by A5, PARTFUN1:def 2;
hence x . i = {} by FUNCT_1:def 2
.= y . i by A6, FUNCT_1:def 2 ;
:: thesis: verum

end;

suppose i in I ; :: thesis: x . i = y . i

then reconsider ii = i as Element of I ;
consider j being Element of I such that
A7: for k being Element of I st k <> j holds
A . k is 1 -element by Def20;

now :: thesis: not j <> indx A

assume j <> indx A ; :: thesis: contradiction
then A . (indx A) is 1 -element by A7;
hence contradiction by Def21; :: thesis: verum

end;

then A . ii is 1 -element by A4, A7;
then consider o being object such that
A8: A . i = {o} by ZFMISC_1:131;
A9: x . ii in A . ii by A1, A3, CARD_3:9;
y . ii in A . ii by A2, A3, CARD_3:9;
hence y . i = o by A8, TARSKI:def 1
.= x . i by A8, A9, TARSKI:def 1 ;
:: thesis: verum

end;

end;