let f, g be ManySortedSet of X; ( ( for i being object holds
( ( b1 . i <= b2 . i implies f . i = b2 . i ) & ( b1 . i > b2 . i implies f . i = b1 . i ) ) ) & ( for i being object holds
( ( b1 . i <= b2 . i implies g . i = b2 . i ) & ( b1 . i > b2 . i implies g . i = b1 . i ) ) ) implies f = g )
assume that
A4:
for i being object holds
( ( b1 . i <= b2 . i implies f . i = b2 . i ) & ( b1 . i > b2 . i implies f . i = b1 . i ) )
and
A5:
for i being object holds
( ( b1 . i <= b2 . i implies g . i = b2 . i ) & ( b1 . i > b2 . i implies g . i = b1 . i ) )
; f = g
hence
f = g
; verum