set f = the ManySortedSet of A;
set g = the ManySortedSet of B;
take [ the ManySortedSet of A, the ManySortedSet of B] ; :: thesis: ex f being ManySortedSet of A ex g being ManySortedSet of B st [ the ManySortedSet of A, the ManySortedSet of B] = [f,g]
take the ManySortedSet of A ; :: thesis: ex g being ManySortedSet of B st [ the ManySortedSet of A, the ManySortedSet of B] = [ the ManySortedSet of A,g]
take the ManySortedSet of B ; :: thesis: [ the ManySortedSet of A, the ManySortedSet of B] = [ the ManySortedSet of A, the ManySortedSet of B]
thus [ the ManySortedSet of A, the ManySortedSet of B] = [ the ManySortedSet of A, the ManySortedSet of B] ; :: thesis: verum