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

now :: thesis: for i being object st i in X holds
f . i = g . i

let i be object ; :: thesis: ( i in X implies f . b₁ = g . b₁ )
assume i in X ; :: thesis: f . b₁ = g . b₁

per cases ( b1 . i <= b2 . i or b1 . i > b2 . i ) ;

suppose A6: b1 . i <= b2 . i ; :: thesis: f . b₁ = g . b₁

hence f . i = b1 . i by A4
.= g . i by A5, A6 ;
:: thesis: verum

end;

suppose A7: b1 . i > b2 . i ; :: thesis: f . b₁ = g . b₁

hence f . i = b2 . i by A4
.= g . i by A5, A7 ;
:: thesis: verum

end;

end;

end;

hence f = g ; :: thesis: verum