let I be non empty set ; for A, B being non trivial-yielding Segre-like ManySortedSet of I st 2 c= card ((product A) /\ (product B)) holds
( indx A = indx B & ( for i being object st i <> indx A holds
A . i = B . i ) )
let A, B be non trivial-yielding Segre-like ManySortedSet of I; ( 2 c= card ((product A) /\ (product B)) implies ( indx A = indx B & ( for i being object st i <> indx A holds
A . i = B . i ) ) )
A1:
dom B = I
by PARTFUN1:def 2;
assume
2 c= card ((product A) /\ (product B))
; ( indx A = indx B & ( for i being object st i <> indx A holds
A . i = B . i ) )
then consider a, b being object such that
A2:
a in (product A) /\ (product B)
and
A3:
b in (product A) /\ (product B)
and
A4:
a <> b
by Th2;
b in product A
by A3, XBOOLE_0:def 4;
then consider b1 being Function such that
A5:
b1 = b
and
A6:
dom b1 = dom A
and
A7:
for o being object st o in dom A holds
b1 . o in A . o
by CARD_3:def 5;
a in product A
by A2, XBOOLE_0:def 4;
then consider a1 being Function such that
A8:
a1 = a
and
A9:
dom a1 = dom A
and
A10:
for o being object st o in dom A holds
a1 . o in A . o
by CARD_3:def 5;
consider o being object such that
A11:
o in dom A
and
A12:
a1 . o <> b1 . o
by A4, A8, A9, A5, A6, FUNCT_1:2;
reconsider o = o as Element of I by A11, PARTFUN1:def 2;
b in product B
by A3, XBOOLE_0:def 4;
then A13:
b1 . o in B . o
by A5, A1, CARD_3:9;
A14:
a in product B
by A2, XBOOLE_0:def 4;
then
a1 . o in B . o
by A8, A1, CARD_3:9;
then
2 c= card (B . o)
by A12, A13, Th2;
then A15:
not B . o is trivial
by Th4;
then A16:
o = indx B
by Def21;
A17:
b1 . o in A . o
by A7, A11;
a1 . o in A . o
by A10, A11;
then
2 c= card (A . o)
by A12, A17, Th2;
then
not A . o is trivial
by Th4;
then A18:
o = indx A
by Def21;
hence
indx A = indx B
by A15, Def21; for i being object st i <> indx A holds
A . i = B . i
let i be object ; ( i <> indx A implies A . i = B . i )
assume A19:
i <> indx A
; A . i = B . i
per cases
( i in I or not i in I )
;
suppose A20:
i in I
;
A . i = B . ithen
B . i is 1
-element
by A18, A16, A19, Th12;
then A21:
ex
y being
object st
B . i = {y}
by ZFMISC_1:131;
A . i is 1
-element
by A19, A20, Th12;
then consider x being
object such that A22:
A . i = {x}
by ZFMISC_1:131;
dom B = I
by PARTFUN1:def 2;
then A23:
a1 . i in B . i
by A8, A14, A20, CARD_3:9;
dom A = I
by PARTFUN1:def 2;
then
a1 . i in A . i
by A10, A20;
then
a1 . i = x
by A22, TARSKI:def 1;
hence
A . i = B . i
by A22, A21, A23, TARSKI:def 1;
verum end;