let I be non empty set ; :: thesis: for A being 1-sorted-yielding ManySortedSet of I

for x being Element of I holds (Carrier A) . x = [#] (A . x)

let A be 1-sorted-yielding ManySortedSet of I; :: thesis: for x being Element of I holds (Carrier A) . x = [#] (A . x)

let x be Element of I; :: thesis: (Carrier A) . x = [#] (A . x)

ex R being 1-sorted st

( R = A . x & (Carrier A) . x = the carrier of R ) by PRALG_1:def 15;

hence (Carrier A) . x = [#] (A . x) ; :: thesis: verum

for x being Element of I holds (Carrier A) . x = [#] (A . x)

let A be 1-sorted-yielding ManySortedSet of I; :: thesis: for x being Element of I holds (Carrier A) . x = [#] (A . x)

let x be Element of I; :: thesis: (Carrier A) . x = [#] (A . x)

ex R being 1-sorted st

( R = A . x & (Carrier A) . x = the carrier of R ) by PRALG_1:def 15;

hence (Carrier A) . x = [#] (A . x) ; :: thesis: verum