let f, g be ManySortedSet of ; :: thesis: ( ( for i being set holds
( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) ) ) & ( for i being set holds
( ( b1 . i <= b2 . i implies g . i = b1 . i ) & ( b1 . i > b2 . i implies g . i = b2 . i ) ) ) implies f = g )
assume that
A2: for i being set holds
( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) ) and
A3: for i being set holds
( ( b1 . i <= b2 . i implies g . i = b1 . i ) & ( b1 . i > b2 . i implies g . i = b2 . i ) ) ; :: thesis: f = g

now

let i be set ; :: 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 A4: b1 . i <= b2 . i ; :: thesis: f . b₁ = g . b₁

hence f . i = b1 . i by A2
.= g . i by A3, A4 ;
:: thesis: verum

end;

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

hence f . i = b2 . i by A2
.= g . i by A3, A5 ;
:: thesis: verum

end;

end;

end;

hence f = g by PBOOLE:3; :: thesis: verum