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 . b1 = g . b1 )
assume i in X ; :: thesis: f . b1 = g . b1
per cases ( b1 . i <= b2 . i or b1 . i > b2 . i ) ;
suppose A6: b1 . i <= b2 . i ; :: thesis: f . b1 = g . b1
hence f . i = b1 . i by A4
.= g . i by A5, A6 ;
:: thesis: verum
end;
suppose A7: b1 . i > b2 . i ; :: thesis: f . b1 = g . b1
hence f . i = b2 . i by A4
.= g . i by A5, A7 ;
:: thesis: verum
end;
end;
end;
hence f = g ; :: thesis: verum