let V1, V2 be ManySortedSet of the carrier of S; :: thesis: ( ( for s being set 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 set 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 set 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 set 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

let s be set ; :: 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 by PBOOLE:3; :: thesis: verum