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