let V1, V2 be ManySortedSet of the carrier of S; :: thesis: ( ( for s being object st s in the carrier of S holds
V1 . s = { (a `1) where a is Element of rng t : a `2 = s } ) & ( for s being object st s in the carrier of S holds
V2 . s = { (a `1) where a is Element of rng t : a `2 = s } ) implies V1 = V2 )
assume that
A1: for s being object st s in the carrier of S holds
V1 . s = { (a `1) where a is Element of rng t : a `2 = s } and
A2: for s being object st s in the carrier of S holds
V2 . s = { (a `1) where a is Element of rng t : a `2 = s } ; :: thesis: V1 = V2

now :: thesis: for s being object st s in the carrier of S holds
V1 . s = V2 . s

let s be object ; :: thesis: ( s in the carrier of S implies V1 . s = V2 . s )
assume A3: s in the carrier of S ; :: thesis: V1 . s = V2 . s
hence V1 . s = { (a `1) where a is Element of rng t : a `2 = s } by A1
.= V2 . s by A2, A3 ;
:: thesis: verum

end;

hence V1 = V2 ; :: thesis: verum