let I be non empty set ; :: thesis: for A being 1-sorted-yielding ManySortedSet of
for x being Element of I holds (Carrier A) . x = [#] (A . x)
let A be 1-sorted-yielding ManySortedSet of ; :: 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)
consider R being 1-sorted such that
A1: ( R = A . x & (Carrier A) . x = the carrier of R ) by PRALG_1:def 13;
thus (Carrier A) . x = [#] (A . x) by A1; :: thesis: verum