let A1, A2 be ManySortedSet of I; ( ( for i being object st i in I holds
A1 . i = (X . i) \/ (Y . i) ) & ( for i being object st i in I holds
A2 . i = (X . i) \/ (Y . i) ) implies A1 = A2 )
assume that
A3:
for i being object st i in I holds
A1 . i = (X . i) \/ (Y . i)
and
A4:
for i being object st i in I holds
A2 . i = (X . i) \/ (Y . i)
; A1 = A2
now for i being object st i in I holds
A1 . i = A2 . ilet i be
object ;
( i in I implies A1 . i = A2 . i )assume A5:
i in I
;
A1 . i = A2 . ihence A1 . i =
(X . i) \/ (Y . i)
by A3
.=
A2 . i
by A4, A5
;
verum end;
hence
A1 = A2
by Th3; verum