let I be set ; for x1, x2, A, B being ManySortedSet of I st x1 is V2() & A is V2() & [|x1,A|] = [|x2,B|] holds
( x1 = x2 & A = B )
let x1, x2, A, B be ManySortedSet of I; ( x1 is V2() & A is V2() & [|x1,A|] = [|x2,B|] implies ( x1 = x2 & A = B ) )
assume that
A1:
x1 is V2()
and
A2:
A is V2()
and
A3:
[|x1,A|] = [|x2,B|]
; ( x1 = x2 & A = B )
hence
x1 = x2
; A = B
hence
A = B
; verum