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

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

hence
V1 = V2
; :: thesis: verumV1 . 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;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