let Y be non empty set ; :: thesis: for J being 1-sorted-yielding ManySortedSet of Y
for i being Element of Y holds (Carrier J) . i = the carrier of (J . i)
let J be 1-sorted-yielding ManySortedSet of Y; :: thesis: for i being Element of Y holds (Carrier J) . i = the carrier of (J . i)
let i be Element of Y; :: thesis: (Carrier J) . i = the carrier of (J . i)
ex R being 1-sorted st
( R = J . i & (Carrier J) . i = the carrier of R ) by PRALG_1:def 15;
hence (Carrier J) . i = the carrier of (J . i) ; :: thesis: verum