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

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

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

then A4: ( not i in dom x & not i in dom y ) by PARTFUN1:def 4;
hence x . i = {} by FUNCT_1:def 4
.= y . i by A4, FUNCT_1:def 4 ;
:: 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
A5: for k being Element of I st k <> j holds
( not A . k is empty & A . k is trivial ) by Def20;

now

assume j <> indx A ; :: thesis: contradiction
then A . (indx A) is trivial by A5;
hence contradiction by Def21; :: thesis: verum

end;

then ( not A . ii is empty & A . ii is trivial ) by A3, A5;
then consider o being set such that
A6: A . i = {o} by REALSET1:def 4;
A7: x . ii in A . ii by A1, A2, CARD_3:18;
y . ii in A . ii by A1, A2, CARD_3:18;
hence y . i = o by A6, TARSKI:def 1
.= x . i by A6, A7, TARSKI:def 1 ;
:: thesis: verum

end;

end;