let I be non empty set ; :: thesis: for A, B being non trivial-yielding Segre-like ManySortedSet of st 2 c= card ((product A) /\ (product B)) holds
( indx A = indx B & ( for i being set st i <> indx A holds
A . i = B . i ) )
let A, B be non trivial-yielding Segre-like ManySortedSet of ; :: thesis: ( 2 c= card ((product A) /\ (product B)) implies ( indx A = indx B & ( for i being set st i <> indx A holds
A . i = B . i ) ) )
assume 2 c= card ((product A) /\ (product B)) ; :: thesis: ( indx A = indx B & ( for i being set st i <> indx A holds
A . i = B . i ) )
then consider a, b being set such that
A1: ( a in (product A) /\ (product B) & b in (product A) /\ (product B) & a <> b ) by Th2;
a in product A by A1, XBOOLE_0:def 4;
then consider a1 being Function such that
A2: ( a1 = a & dom a1 = dom A & ( for o being set st o in dom A holds
a1 . o in A . o ) ) by CARD_3:def 5;
A3: a in product B by A1, XBOOLE_0:def 4;
b in product A by A1, XBOOLE_0:def 4;
then consider b1 being Function such that
A4: ( b1 = b & dom b1 = dom A & ( for o being set st o in dom A holds
b1 . o in A . o ) ) by CARD_3:def 5;
A5: b in product B by A1, XBOOLE_0:def 4;
consider o being set such that
A6: ( o in dom A & a1 . o <> b1 . o ) by A1, A2, A4, FUNCT_1:9;
reconsider o = o as Element of I by A6, PARTFUN1:def 4;
( a1 . o in A . o & b1 . o in A . o ) by A2, A4, A6;
then 2 c= card (A . o) by A6, Th2;
then not A . o is trivial by Th4;
then A7: o = indx A by Def21;
dom B = I by PARTFUN1:def 4;
then ( a1 . o in B . o & b1 . o in B . o ) by A2, A3, A4, A5, CARD_3:18;
then 2 c= card (B . o) by A6, Th2;
then A8: not B . o is trivial by Th4;
then A9: o = indx B by Def21;
thus indx A = indx B by A7, A8, Def21; :: thesis: for i being set st i <> indx A holds
A . i = B . i
let i be set ; :: thesis: ( i <> indx A implies A . i = B . i )
assume A10: i <> indx A ; :: thesis: A . i = B . i

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

suppose A11: i in I ; :: thesis: A . i = B . i

then A12: ( not A . i is empty & A . i is trivial & not B . i is empty & B . i is trivial ) by A7, A9, A10, Th12;
then consider x being set such that
A13: A . i = {x} by REALSET1:def 4;
consider y being set such that
A14: B . i = {y} by A12, REALSET1:def 4;
dom A = I by PARTFUN1:def 4;
then a1 . i in A . i by A2, A11;
then A15: a1 . i = x by A13, TARSKI:def 1;
dom B = I by PARTFUN1:def 4;
then a1 . i in B . i by A2, A3, A11, CARD_3:18;
hence A . i = B . i by A13, A14, A15, TARSKI:def 1; :: thesis: verum

end;

suppose not i in I ; :: thesis: A . i = B . i

then A16: ( not i in dom A & not i in dom B ) by PARTFUN1:def 4;
hence A . i = {} by FUNCT_1:def 4
.= B . i by A16, FUNCT_1:def 4 ;
:: thesis: verum

end;

end;